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

.= ([: 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

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

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

.= ([: 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