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

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;

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 ((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:] )
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;

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

end;

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

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

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

proof
end;

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

end;

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;hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by XBOOLE_0:def 3; :: thesis: verum

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

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;

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;hence a in [: the carrier of G, the carrier of G:] ; :: thesis: verum