hereby :: thesis: ( not E c= the_Edges_of G implies ex b₁ being _Graph st b₁ == G )

assume E c= the_Edges_of G ; :: thesis: ex G1 being set st
( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of G1 = (the_Target_of G) +* ((the_Source_of G) | E) )
set V = the_Vertices_of G;
set E1 = the_Edges_of G;
set S = (the_Source_of G) +* ((the_Target_of G) | E);
reconsider S = (the_Source_of G) +* ((the_Target_of G) | E) as Function of (the_Edges_of G),(the_Vertices_of G) ;
set T = (the_Target_of G) +* ((the_Source_of G) | E);
reconsider T = (the_Target_of G) +* ((the_Source_of G) | E) as Function of (the_Edges_of G),(the_Vertices_of G) ;
set G1 = createGraph ((the_Vertices_of G),(the_Edges_of G),S,T);
take G1 = createGraph ((the_Vertices_of G),(the_Edges_of G),S,T); :: thesis: ( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of G1 = (the_Target_of G) +* ((the_Source_of G) | E) )
thus ( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of G1 = (the_Target_of G) +* ((the_Source_of G) | E) ) ; :: thesis: verum

end;

assume not E c= the_Edges_of G ; :: thesis: ex b₁ being _Graph st b₁ == G
take G ; :: thesis: G == G
thus G == G ; :: thesis: verum