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