let G be strict irreflexive RelStr ; :: thesis: ComplRelStr (ComplRelStr G) = G
set CCmpG = ComplRelStr (ComplRelStr G);
set CmpG = ComplRelStr G;
set cG = the carrier of G;
set IG = the InternalRel of G;
set ICmpG = the InternalRel of (ComplRelStr G);
set ICCmpG = the InternalRel of (ComplRelStr (ComplRelStr G));
A1: the carrier of G = the carrier of (ComplRelStr G) by NECKLACE:def 8
.= the carrier of (ComplRelStr (ComplRelStr G)) by NECKLACE:def 8 ;
A2: the carrier of G = the carrier of (ComplRelStr G) 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 A4, XBOOLE_0:def 4;
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 A4, RELSET_1:2;
a in id the carrier of G by A4, XBOOLE_0:def 4;
then x = y by A6, RELAT_1:def 10;
hence contradiction by A5, A6, A7, NECKLACE:def 5; :: thesis: verum

end;

the InternalRel of (ComplRelStr (ComplRelStr G)) = ( the InternalRel of (ComplRelStr G) `) \ (id the carrier of (ComplRelStr G)) by NECKLACE:def 8
.= ([: the carrier of (ComplRelStr G), the carrier of (ComplRelStr G):] \ the InternalRel of (ComplRelStr G)) \ (id the carrier of (ComplRelStr G)) 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 A2, NECKLACE:def 8
.= (([: 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 A3, XBOOLE_1:83 ;
hence ComplRelStr (ComplRelStr G) = G by A1; :: thesis: verum