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 set ; :: 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 set such that
A2: ( x in the carrier of G & y in the carrier of G & a = [x,y] ) by ZFMISC_1:def 2;

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

suppose A3: 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 A2, A3, 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 A4: not a in id the carrier of G by A2, 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 5;
then a in (the InternalRel of G ` ) \ (id the carrier of G) by A4, XBOOLE_0:def 5;
then a in the InternalRel of (ComplRelStr G) by NECKLACE:def 9;
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 set ; :: 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 A5: ( 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 A5, XBOOLE_0:def 3;

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

then consider x, y being set such that
A6: ( a = [x,y] & x in the carrier of G & y in the carrier of G ) by RELSET_1:6;
thus a in [:the carrier of G,the carrier of G:] by A6, ZFMISC_1:106; :: thesis: verum

end;

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

then consider x, y being set such that
A7: ( a = [x,y] & x in the carrier of G & y in the carrier of G ) by RELSET_1:6;
thus a in [:the carrier of G,the carrier of G:] by A7, ZFMISC_1:106; :: 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 9;
hence a in [:the carrier of G,the carrier of G:] ; :: thesis: verum

end;

end;