let G, H be _Graph; :: thesis: ( the_Vertices_of {G,H} = {(the_Vertices_of G),(the_Vertices_of H)} & the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} & the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

now :: thesis: for x being object holds
( ( x in the_Vertices_of {G,H} implies x in {(the_Vertices_of G),(the_Vertices_of H)} ) & ( x in {(the_Vertices_of G),(the_Vertices_of H)} implies x in the_Vertices_of {G,H} ) )

let x be object ; :: thesis: ( ( x in the_Vertices_of {G,H} implies x in {(the_Vertices_of G),(the_Vertices_of H)} ) & ( x in {(the_Vertices_of G),(the_Vertices_of H)} implies x in the_Vertices_of {G,H} ) )

hereby :: thesis: ( x in {(the_Vertices_of G),(the_Vertices_of H)} implies x in the_Vertices_of {G,H} )

assume x in the_Vertices_of {G,H} ; :: thesis: x in {(the_Vertices_of G),(the_Vertices_of H)}
then consider G0 being Element of {G,H} such that
A1: x = the_Vertices_of G0 ;

per cases ( G0 = G or G0 = H ) by TARSKI:def 2;

suppose G0 = G ; :: thesis: x in {(the_Vertices_of G),(the_Vertices_of H)}

hence x in {(the_Vertices_of G),(the_Vertices_of H)} by A1, TARSKI:def 2; :: thesis: verum

end;

suppose G0 = H ; :: thesis: x in {(the_Vertices_of G),(the_Vertices_of H)}

hence x in {(the_Vertices_of G),(the_Vertices_of H)} by A1, TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume x in {(the_Vertices_of G),(the_Vertices_of H)} ; :: thesis: x in the_Vertices_of {G,H}
then A2: ( x = the_Vertices_of G or x = the_Vertices_of H ) by TARSKI:def 2;
( G in {G,H} & H in {G,H} ) by TARSKI:def 2;
hence x in the_Vertices_of {G,H} by A2; :: thesis: verum

end;

hence the_Vertices_of {G,H} = {(the_Vertices_of G),(the_Vertices_of H)} by TARSKI:2; :: thesis: ( the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} & the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

now :: thesis: for x being object holds
( ( x in the_Edges_of {G,H} implies x in {(the_Edges_of G),(the_Edges_of H)} ) & ( x in {(the_Edges_of G),(the_Edges_of H)} implies x in the_Edges_of {G,H} ) )

let x be object ; :: thesis: ( ( x in the_Edges_of {G,H} implies x in {(the_Edges_of G),(the_Edges_of H)} ) & ( x in {(the_Edges_of G),(the_Edges_of H)} implies x in the_Edges_of {G,H} ) )

hereby :: thesis: ( x in {(the_Edges_of G),(the_Edges_of H)} implies x in the_Edges_of {G,H} )

assume x in the_Edges_of {G,H} ; :: thesis: x in {(the_Edges_of G),(the_Edges_of H)}
then consider G0 being Element of {G,H} such that
A3: x = the_Edges_of G0 ;

per cases ( G0 = G or G0 = H ) by TARSKI:def 2;

suppose G0 = G ; :: thesis: x in {(the_Edges_of G),(the_Edges_of H)}

hence x in {(the_Edges_of G),(the_Edges_of H)} by A3, TARSKI:def 2; :: thesis: verum

end;

suppose G0 = H ; :: thesis: x in {(the_Edges_of G),(the_Edges_of H)}

hence x in {(the_Edges_of G),(the_Edges_of H)} by A3, TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume x in {(the_Edges_of G),(the_Edges_of H)} ; :: thesis: x in the_Edges_of {G,H}
then A4: ( x = the_Edges_of G or x = the_Edges_of H ) by TARSKI:def 2;
( G in {G,H} & H in {G,H} ) by TARSKI:def 2;
hence x in the_Edges_of {G,H} by A4; :: thesis: verum

end;

hence the_Edges_of {G,H} = {(the_Edges_of G),(the_Edges_of H)} by TARSKI:2; :: thesis: ( the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} & the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} )

now :: thesis: for x being object holds
( ( x in the_Source_of {G,H} implies x in {(the_Source_of G),(the_Source_of H)} ) & ( x in {(the_Source_of G),(the_Source_of H)} implies x in the_Source_of {G,H} ) )

let x be object ; :: thesis: ( ( x in the_Source_of {G,H} implies x in {(the_Source_of G),(the_Source_of H)} ) & ( x in {(the_Source_of G),(the_Source_of H)} implies x in the_Source_of {G,H} ) )

hereby :: thesis: ( x in {(the_Source_of G),(the_Source_of H)} implies x in the_Source_of {G,H} )

assume x in the_Source_of {G,H} ; :: thesis: x in {(the_Source_of G),(the_Source_of H)}
then consider G0 being Element of {G,H} such that
A5: x = the_Source_of G0 ;

per cases ( G0 = G or G0 = H ) by TARSKI:def 2;

suppose G0 = G ; :: thesis: x in {(the_Source_of G),(the_Source_of H)}

hence x in {(the_Source_of G),(the_Source_of H)} by A5, TARSKI:def 2; :: thesis: verum

end;

suppose G0 = H ; :: thesis: x in {(the_Source_of G),(the_Source_of H)}

hence x in {(the_Source_of G),(the_Source_of H)} by A5, TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume x in {(the_Source_of G),(the_Source_of H)} ; :: thesis: x in the_Source_of {G,H}
then A6: ( x = the_Source_of G or x = the_Source_of H ) by TARSKI:def 2;
( G in {G,H} & H in {G,H} ) by TARSKI:def 2;
hence x in the_Source_of {G,H} by A6; :: thesis: verum

end;

hence the_Source_of {G,H} = {(the_Source_of G),(the_Source_of H)} by TARSKI:2; :: thesis: the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)}

now :: thesis: for x being object holds
( ( x in the_Target_of {G,H} implies x in {(the_Target_of G),(the_Target_of H)} ) & ( x in {(the_Target_of G),(the_Target_of H)} implies x in the_Target_of {G,H} ) )

let x be object ; :: thesis: ( ( x in the_Target_of {G,H} implies x in {(the_Target_of G),(the_Target_of H)} ) & ( x in {(the_Target_of G),(the_Target_of H)} implies x in the_Target_of {G,H} ) )

hereby :: thesis: ( x in {(the_Target_of G),(the_Target_of H)} implies x in the_Target_of {G,H} )

assume x in the_Target_of {G,H} ; :: thesis: x in {(the_Target_of G),(the_Target_of H)}
then consider G0 being Element of {G,H} such that
A7: x = the_Target_of G0 ;

per cases ( G0 = G or G0 = H ) by TARSKI:def 2;

suppose G0 = G ; :: thesis: x in {(the_Target_of G),(the_Target_of H)}

hence x in {(the_Target_of G),(the_Target_of H)} by A7, TARSKI:def 2; :: thesis: verum

end;

suppose G0 = H ; :: thesis: x in {(the_Target_of G),(the_Target_of H)}

hence x in {(the_Target_of G),(the_Target_of H)} by A7, TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume x in {(the_Target_of G),(the_Target_of H)} ; :: thesis: x in the_Target_of {G,H}
then A8: ( x = the_Target_of G or x = the_Target_of H ) by TARSKI:def 2;
( G in {G,H} & H in {G,H} ) by TARSKI:def 2;
hence x in the_Target_of {G,H} by A8; :: thesis: verum

end;

hence the_Target_of {G,H} = {(the_Target_of G),(the_Target_of H)} by TARSKI:2; :: thesis: verum