The final stages of the proof.
%%lemma('Ground Reducible Graph').%%lemma('Reducible Graph').
rdf:List
.
Hence, if b were the object of
a triple with a uriref subject, we can apply either
the
%%linkLemma('GGB Triple Reduction').
or the
%%linkLemma('blank explicit type reduction').
.
Thus, by the %%linkLemma('blank node'). ,
without loss of generality, we have that b is
not the object of any triple.
rdf:List
, it must be of
category
unnamedIndividual, allDifferent,
%%dl_only(Lvl,'unnamedDataRange, ').
%%dl_only(Lvl,'description, ').
or restriction.
By the %%linkLemma('unnamed individual').
the first possibility is excluded.
%%dl_only(Lvl,'Since the ').
%%Lvl=dl->linkLemma('Description Comparison Reduction');true.
%%dl_only(Lvl,'does not apply, b is not the subject of a triple
with predicate owl:disjointWith
,
or owl:equivalentClass
.').
The conditions on b and g
now meet the premises of the
%%Lvl=dl->linkLemma('Structured Nodes');linkLemma('first structure reduction').
and so g is, after all, reducible.
We now can prove the main results: