let S1, S2 be Graph-membered set ; :: thesis:

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Vertices_of (S1 \/ S2) ; :: thesis:
then consider G being _Graph such that
A1: ( G in S1 \/ S2 & x = the_Vertices_of G ) by Def14;

per cases by A1, XBOOLE_0:def 3;

suppose G in S1 ; :: thesis:

then x in the_Vertices_of S1 by A1, Def14;
hence x in (the_Vertices_of S1) \/ (the_Vertices_of S2) by XBOOLE_0:def 3; :: thesis:

end;

suppose G in S2 ; :: thesis:

then x in the_Vertices_of S2 by A1, Def14;
hence x in (the_Vertices_of S1) \/ (the_Vertices_of S2) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (the_Vertices_of S1) \/ (the_Vertices_of S2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in the_Vertices_of S1 ; :: thesis:

then consider G being _Graph such that
A2: ( G in S1 & x = the_Vertices_of G ) by Def14;
G in S1 \/ S2 by A2, XBOOLE_0:def 3;
hence x in the_Vertices_of (S1 \/ S2) by A2, Def14; :: thesis:

end;

suppose x in the_Vertices_of S2 ; :: thesis:

then consider G being _Graph such that
A3: ( G in S2 & x = the_Vertices_of G ) by Def14;
G in S1 \/ S2 by A3, XBOOLE_0:def 3;
hence x in the_Vertices_of (S1 \/ S2) by A3, Def14; :: thesis:

end;

end;

end;

hence the_Vertices_of (S1 \/ S2) = (the_Vertices_of S1) \/ (the_Vertices_of S2) by TARSKI:2; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Edges_of (S1 \/ S2) ; :: thesis:
then consider G being _Graph such that
A4: ( G in S1 \/ S2 & x = the_Edges_of G ) by Def15;

per cases by A4, XBOOLE_0:def 3;

suppose G in S1 ; :: thesis:

then x in the_Edges_of S1 by A4, Def15;
hence x in (the_Edges_of S1) \/ (the_Edges_of S2) by XBOOLE_0:def 3; :: thesis:

end;

suppose G in S2 ; :: thesis:

then x in the_Edges_of S2 by A4, Def15;
hence x in (the_Edges_of S1) \/ (the_Edges_of S2) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (the_Edges_of S1) \/ (the_Edges_of S2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in the_Edges_of S1 ; :: thesis:

then consider G being _Graph such that
A5: ( G in S1 & x = the_Edges_of G ) by Def15;
G in S1 \/ S2 by A5, XBOOLE_0:def 3;
hence x in the_Edges_of (S1 \/ S2) by A5, Def15; :: thesis:

end;

suppose x in the_Edges_of S2 ; :: thesis:

then consider G being _Graph such that
A6: ( G in S2 & x = the_Edges_of G ) by Def15;
G in S1 \/ S2 by A6, XBOOLE_0:def 3;
hence x in the_Edges_of (S1 \/ S2) by A6, Def15; :: thesis:

end;

end;

end;

hence the_Edges_of (S1 \/ S2) = (the_Edges_of S1) \/ (the_Edges_of S2) by TARSKI:2; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Source_of (S1 \/ S2) ; :: thesis:
then consider G being _Graph such that
A7: ( G in S1 \/ S2 & x = the_Source_of G ) by Def16;

per cases by A7, XBOOLE_0:def 3;

suppose G in S1 ; :: thesis:

then x in the_Source_of S1 by A7, Def16;
hence x in (the_Source_of S1) \/ (the_Source_of S2) by XBOOLE_0:def 3; :: thesis:

end;

suppose G in S2 ; :: thesis:

then x in the_Source_of S2 by A7, Def16;
hence x in (the_Source_of S1) \/ (the_Source_of S2) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (the_Source_of S1) \/ (the_Source_of S2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in the_Source_of S1 ; :: thesis:

then consider G being _Graph such that
A8: ( G in S1 & x = the_Source_of G ) by Def16;
G in S1 \/ S2 by A8, XBOOLE_0:def 3;
hence x in the_Source_of (S1 \/ S2) by A8, Def16; :: thesis:

end;

suppose x in the_Source_of S2 ; :: thesis:

then consider G being _Graph such that
A9: ( G in S2 & x = the_Source_of G ) by Def16;
G in S1 \/ S2 by A9, XBOOLE_0:def 3;
hence x in the_Source_of (S1 \/ S2) by A9, Def16; :: thesis:

end;

end;

end;

hence the_Source_of (S1 \/ S2) = (the_Source_of S1) \/ (the_Source_of S2) by TARSKI:2; :: thesis:

end;

hereby :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Target_of (S1 \/ S2) ; :: thesis:
then consider G being _Graph such that
A10: ( G in S1 \/ S2 & x = the_Target_of G ) by Def17;

per cases by A10, XBOOLE_0:def 3;

suppose G in S1 ; :: thesis:

then x in the_Target_of S1 by A10, Def17;
hence x in (the_Target_of S1) \/ (the_Target_of S2) by XBOOLE_0:def 3; :: thesis:

end;

suppose G in S2 ; :: thesis:

then x in the_Target_of S2 by A10, Def17;
hence x in (the_Target_of S1) \/ (the_Target_of S2) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (the_Target_of S1) \/ (the_Target_of S2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in the_Target_of S1 ; :: thesis:

then consider G being _Graph such that
A11: ( G in S1 & x = the_Target_of G ) by Def17;
G in S1 \/ S2 by A11, XBOOLE_0:def 3;
hence x in the_Target_of (S1 \/ S2) by A11, Def17; :: thesis:

end;

suppose x in the_Target_of S2 ; :: thesis:

then consider G being _Graph such that
A12: ( G in S2 & x = the_Target_of G ) by Def17;
G in S1 \/ S2 by A12, XBOOLE_0:def 3;
hence x in the_Target_of (S1 \/ S2) by A12, Def17; :: thesis:

end;

end;

end;

hence the_Target_of (S1 \/ S2) = (the_Target_of S1) \/ (the_Target_of S2) by TARSKI:2; :: thesis:

end;