let G be strict irreflexive RelStr ; :: thesis: ( G is trivial implies ComplRelStr G = G )
set CG = ComplRelStr G;
assume G is trivial ; :: thesis: ComplRelStr G = G
then A1: the carrier of G is trivial ;

per cases ( the carrier of G is empty or ex x being set st the carrier of G = {x} ) by A1, REALSET1:def 4;

suppose A2: the carrier of G is empty ; :: thesis: ComplRelStr G = G

then the InternalRel of G c= [:{} ,{} :] ;
then A3: the InternalRel of G c= {} ;
A4: the InternalRel of G = {} by A3;
the InternalRel of (ComplRelStr G) = (the InternalRel of G ` ) \ (id the carrier of G) by NECKLACE:def 9;
then the InternalRel of (ComplRelStr G) = ([:{} ,{} :] \ {} ) \ (id {} ) by A2;
then the InternalRel of (ComplRelStr G) = ({} \ {} ) \ (id {} ) ;
hence ComplRelStr G = G by A4, NECKLACE:def 9; :: thesis: verum

end;

suppose ex x being set st the carrier of G = {x} ; :: thesis: ComplRelStr G = G

then consider x being set such that
A5: the carrier of G = {x} ;
the InternalRel of G c= [:{x},{x}:] by A5;
then the InternalRel of G c= {[x,x]} by ZFMISC_1:35;
then A6: ( the InternalRel of G = {} or the InternalRel of G = {[x,x]} ) by ZFMISC_1:39;
A7: the InternalRel of G <> {[x,x]}

proof

assume not the InternalRel of G <> {[x,x]} ; :: thesis: contradiction
then A8: [x,x] in the InternalRel of G by TARSKI:def 1;
x in the carrier of G by A5, TARSKI:def 1;
hence contradiction by A8, NECKLACE:def 6; :: thesis: verum

end;

A9: the carrier of (ComplRelStr G) = {x} by A5, NECKLACE:def 9;
the InternalRel of (ComplRelStr G) = (the InternalRel of G ` ) \ (id the carrier of G) by NECKLACE:def 9;
then the InternalRel of (ComplRelStr G) = ([:{x},{x}:] \ {} ) \ (id {x}) by A5, A6, A7, SUBSET_1:def 5;
then the InternalRel of (ComplRelStr G) = {[x,x]} \ (id {x}) by ZFMISC_1:35;
then the InternalRel of (ComplRelStr G) = {[x,x]} \ {[x,x]} by SYSREL:30;
hence ComplRelStr G = G by A5, A6, A7, A9, XBOOLE_1:37; :: thesis: verum

end;

end;