let G be strict irreflexive RelStr ; :: thesis:
set CCmpG = ComplRelStr ();
set CmpG = ComplRelStr G;
set cG = the carrier of G;
set IG = the InternalRel of G;
set ICmpG = the InternalRel of ();
set ICCmpG = the InternalRel of ();
A1: the carrier of G = the carrier of () by NECKLACE:def 8
.= the carrier of () by NECKLACE:def 8 ;
A2: the carrier of G = the carrier of () by NECKLACE:def 8;
A3: id the carrier of G misses the InternalRel of G
proof
assume not id the carrier of G misses the InternalRel of G ; :: thesis: contradiction
then (id the carrier of G) /\ the InternalRel of G <> {} ;
then consider a being object such that
A4: a in (id the carrier of G) /\ the InternalRel of G by XBOOLE_0:def 1;
A5: a in the InternalRel of G by ;
consider x, y being object such that
A6: a = [x,y] and
A7: x in the carrier of G and
y in the carrier of G by ;
a in id the carrier of G by ;
then x = y by ;
hence contradiction by A5, A6, A7, NECKLACE:def 5; :: thesis: verum
end;
the InternalRel of () = ( the InternalRel of () `) \ (id the carrier of ()) by NECKLACE:def 8
.= ([: the carrier of (), the carrier of ():] \ the InternalRel of ()) \ (id the carrier of ()) by SUBSET_1:def 4
.= ([: the carrier of G, the carrier of G:] \ (( the InternalRel of G `) \ (id the carrier of G))) \ (id the carrier of G) by
.= (([: the carrier of G, the carrier of G:] \ ( the InternalRel of G `)) \/ ([: the carrier of G, the carrier of G:] /\ (id the carrier of G))) \ (id the carrier of G) by XBOOLE_1:52
.= (([: the carrier of G, the carrier of G:] \ ( the InternalRel of G `)) \/ (id the carrier of G)) \ (id the carrier of G) by XBOOLE_1:28
.= ([: the carrier of G, the carrier of G:] \ ( the InternalRel of G `)) \ (id the carrier of G) by XBOOLE_1:40
.= ([: the carrier of G, the carrier of G:] \ ([: the carrier of G, the carrier of G:] \ the InternalRel of G)) \ (id the carrier of G) by SUBSET_1:def 4
.= ([: the carrier of G, the carrier of G:] /\ the InternalRel of G) \ (id the carrier of G) by XBOOLE_1:48
.= the InternalRel of G \ (id the carrier of G) by XBOOLE_1:28
.= the InternalRel of G by ;
hence ComplRelStr () = G by A1; :: thesis: verum