let G be strict irreflexive RelStr ; 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 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; verum