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

per cases ( the carrier of G is empty or ex x being object st the carrier of G = {x} ) by A1, ZFMISC_1:131;

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

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

end;

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

then consider x being object such that
A4: the carrier of G = {x} ;
A5: the carrier of (ComplRelStr G) = {x} by A4, NECKLACE:def 8;
the InternalRel of G c= [:{x},{x}:] by A4;
then the InternalRel of G c= {[x,x]} by ZFMISC_1:29;
then A6: ( the InternalRel of G = {} or the InternalRel of G = {[x,x]} ) by ZFMISC_1:33;
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 A4, TARSKI:def 1;
hence contradiction by A8, NECKLACE:def 5; :: thesis: verum

end;

the InternalRel of (ComplRelStr G) = ( the InternalRel of G `) \ (id the carrier of G) by NECKLACE:def 8;
then the InternalRel of (ComplRelStr G) = ([:{x},{x}:] \ {}) \ (id {x}) by A4, A6, A7, SUBSET_1:def 4;
then the InternalRel of (ComplRelStr G) = {[x,x]} \ (id {x}) by ZFMISC_1:29;
then the InternalRel of (ComplRelStr G) = {[x,x]} \ {[x,x]} by SYSREL:13;
hence ComplRelStr G = G by A4, A6, A7, A5, XBOOLE_1:37; :: thesis: verum

end;

end;