let G be RelStr ; :: thesis: [: the carrier of G, the carrier of G:] = ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)
set idcG = id the carrier of G;
set IG = the InternalRel of G;
set ICmpG = the InternalRel of (ComplRelStr G);
set cG = the carrier of G;
thus [: the carrier of G, the carrier of G:] c= ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) :: according to XBOOLE_0:def 10 :: thesis: ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) c= [: the carrier of G, the carrier of G:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [: the carrier of G, the carrier of G:] or a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) )
assume A1: a in [: the carrier of G, the carrier of G:] ; :: thesis: a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)
then consider x, y being object such that
A2: x in the carrier of G and
y in the carrier of G and
A3: a = [x,y] by ZFMISC_1:def 2;

per cases ( x = y or x <> y ) ;

suppose A4: x = y ; :: thesis: a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

[x,x] in id the carrier of G by A2, RELAT_1:def 10;
then a in (id the carrier of G) \/ the InternalRel of G by A3, A4, XBOOLE_0:def 3;
hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x <> y ; :: thesis: a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

then A5: not a in id the carrier of G by A3, RELAT_1:def 10;
thus a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) :: thesis: verum

proof

per cases ( a in the InternalRel of G or not a in the InternalRel of G ) ;

suppose a in the InternalRel of G ; :: thesis: a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

then a in (id the carrier of G) \/ the InternalRel of G by XBOOLE_0:def 3;
hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not a in the InternalRel of G ; :: thesis: a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G)

then a in [: the carrier of G, the carrier of G:] \ the InternalRel of G by A1, XBOOLE_0:def 5;
then a in the InternalRel of G ` by SUBSET_1:def 4;
then a in ( the InternalRel of G `) \ (id the carrier of G) by A5, XBOOLE_0:def 5;
then a in the InternalRel of (ComplRelStr G) by NECKLACE:def 8;
then a in the InternalRel of G \/ the InternalRel of (ComplRelStr G) by XBOOLE_0:def 3;
then a in (id the carrier of G) \/ ( the InternalRel of G \/ the InternalRel of (ComplRelStr G)) by XBOOLE_0:def 3;
hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by XBOOLE_1:4; :: thesis: verum

end;

end;

end;

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) or a in [: the carrier of G, the carrier of G:] )
assume a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) ; :: thesis: a in [: the carrier of G, the carrier of G:]
then A6: ( a in (id the carrier of G) \/ the InternalRel of G or a in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

per cases ( a in id the carrier of G or a in the InternalRel of G or a in the InternalRel of (ComplRelStr G) ) by A6, XBOOLE_0:def 3;

suppose a in id the carrier of G ; :: thesis: a in [: the carrier of G, the carrier of G:]

hence a in [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;

suppose a in the InternalRel of G ; :: thesis: a in [: the carrier of G, the carrier of G:]

hence a in [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;

suppose a in the InternalRel of (ComplRelStr G) ; :: thesis: a in [: the carrier of G, the carrier of G:]

then a in ( the InternalRel of G `) \ (id the carrier of G) by NECKLACE:def 8;
hence a in [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;

end;