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 ()
set idcG = id the carrier of G;
set IG = the InternalRel of G;
set ICmpG = the InternalRel of ();
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 () :: according to XBOOLE_0:def 10 :: thesis: ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () )
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 ()
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 ()
[x,x] in id the carrier of G by ;
then a in (id the carrier of G) \/ the InternalRel of G by ;
hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 ()
then A5: not a in id the carrier of G by ;
thus a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () :: 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 ()
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 () 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 ()
then a in [: the carrier of G, the carrier of G:] \ the InternalRel of G by ;
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 ;
then a in the InternalRel of () by NECKLACE:def 8;
then a in the InternalRel of G \/ the InternalRel of () by XBOOLE_0:def 3;
then a in (id the carrier of G) \/ ( the InternalRel of G \/ the InternalRel of ()) by XBOOLE_0:def 3;
hence a in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () 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 () ; :: 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 () ) 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 () ) by ;
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 () ; :: 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;