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

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;

end;

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;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

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]}

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;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

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

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