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 9
.= the carrier of (ComplRelStr (ComplRelStr G)) by NECKLACE:def 9 ;
A2: the carrier of G = the carrier of (ComplRelStr G) by NECKLACE:def 9;
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 <> {} by XBOOLE_0:def 7;
then consider a being set 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 set 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:6;
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 6; :: thesis: verum

end;

the InternalRel of (ComplRelStr (ComplRelStr G)) = (the InternalRel of (ComplRelStr G) ` ) \ (id the carrier of (ComplRelStr G)) by NECKLACE:def 9
.= ([: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 5
.= ([: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 9
.= (([: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 5
.= ([: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