let S1, S2 be Graph-membered set ; :: thesis: ( the_Vertices_of (S1 /\ S2) c= (the_Vertices_of S1) /\ (the_Vertices_of S2) & the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) & the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )
hereby :: thesis: ( the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) & the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )
now :: thesis: for x being object st x in the_Vertices_of (S1 /\ S2) holds
x in (the_Vertices_of S1) /\ (the_Vertices_of S2)
let x be object ; :: thesis: ( x in the_Vertices_of (S1 /\ S2) implies x in (the_Vertices_of S1) /\ (the_Vertices_of S2) )
assume x in the_Vertices_of (S1 /\ S2) ; :: thesis: x in (the_Vertices_of S1) /\ (the_Vertices_of S2)
then consider G being _Graph such that
A1: ( G in S1 /\ S2 & x = the_Vertices_of G ) by Def14;
( G in S1 & G in S2 ) by A1, XBOOLE_0:def 4;
then ( x in the_Vertices_of S1 & x in the_Vertices_of S2 ) by A1, Def14;
hence x in (the_Vertices_of S1) /\ (the_Vertices_of S2) by XBOOLE_0:def 4; :: thesis: verum
end;
hence the_Vertices_of (S1 /\ S2) c= (the_Vertices_of S1) /\ (the_Vertices_of S2) by TARSKI:def 3; :: thesis: verum
end;
hereby :: thesis: ( the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) & the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) )
now :: thesis: for x being object st x in the_Edges_of (S1 /\ S2) holds
x in (the_Edges_of S1) /\ (the_Edges_of S2)
let x be object ; :: thesis: ( x in the_Edges_of (S1 /\ S2) implies x in (the_Edges_of S1) /\ (the_Edges_of S2) )
assume x in the_Edges_of (S1 /\ S2) ; :: thesis: x in (the_Edges_of S1) /\ (the_Edges_of S2)
then consider G being _Graph such that
A2: ( G in S1 /\ S2 & x = the_Edges_of G ) by Def15;
( G in S1 & G in S2 ) by A2, XBOOLE_0:def 4;
then ( x in the_Edges_of S1 & x in the_Edges_of S2 ) by A2, Def15;
hence x in (the_Edges_of S1) /\ (the_Edges_of S2) by XBOOLE_0:def 4; :: thesis: verum
end;
hence the_Edges_of (S1 /\ S2) c= (the_Edges_of S1) /\ (the_Edges_of S2) by TARSKI:def 3; :: thesis: verum
end;
hereby :: thesis: the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2)
now :: thesis: for x being object st x in the_Source_of (S1 /\ S2) holds
x in (the_Source_of S1) /\ (the_Source_of S2)
let x be object ; :: thesis: ( x in the_Source_of (S1 /\ S2) implies x in (the_Source_of S1) /\ (the_Source_of S2) )
assume x in the_Source_of (S1 /\ S2) ; :: thesis: x in (the_Source_of S1) /\ (the_Source_of S2)
then consider G being _Graph such that
A3: ( G in S1 /\ S2 & x = the_Source_of G ) by Def16;
( G in S1 & G in S2 ) by A3, XBOOLE_0:def 4;
then ( x in the_Source_of S1 & x in the_Source_of S2 ) by A3, Def16;
hence x in (the_Source_of S1) /\ (the_Source_of S2) by XBOOLE_0:def 4; :: thesis: verum
end;
hence the_Source_of (S1 /\ S2) c= (the_Source_of S1) /\ (the_Source_of S2) by TARSKI:def 3; :: thesis: verum
end;
hereby :: thesis: verum
now :: thesis: for x being object st x in the_Target_of (S1 /\ S2) holds
x in (the_Target_of S1) /\ (the_Target_of S2)
let x be object ; :: thesis: ( x in the_Target_of (S1 /\ S2) implies x in (the_Target_of S1) /\ (the_Target_of S2) )
assume x in the_Target_of (S1 /\ S2) ; :: thesis: x in (the_Target_of S1) /\ (the_Target_of S2)
then consider G being _Graph such that
A4: ( G in S1 /\ S2 & x = the_Target_of G ) by Def17;
( G in S1 & G in S2 ) by A4, XBOOLE_0:def 4;
then ( x in the_Target_of S1 & x in the_Target_of S2 ) by A4, Def17;
hence x in (the_Target_of S1) /\ (the_Target_of S2) by XBOOLE_0:def 4; :: thesis: verum
end;
hence the_Target_of (S1 /\ S2) c= (the_Target_of S1) /\ (the_Target_of S2) by TARSKI:def 3; :: thesis: verum
end;