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

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

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

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

assume x in the_Vertices_of {G} ; :: thesis: x = the_Vertices_of G
then consider G0 being Element of {G} such that
A1: x = the_Vertices_of G0 ;
thus x = the_Vertices_of G by A1, TARSKI:def 1; :: thesis: verum

end;

assume A2: x = the_Vertices_of G ; :: thesis: x in the_Vertices_of {G}
G in {G} by TARSKI:def 1;
hence x in the_Vertices_of {G} by A2; :: thesis: verum

end;

hence the_Vertices_of {G} = {(the_Vertices_of G)} by TARSKI:def 1; :: thesis: ( the_Edges_of {G} = {(the_Edges_of G)} & the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )

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

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

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

assume x in the_Edges_of {G} ; :: thesis: x = the_Edges_of G
then consider G0 being Element of {G} such that
A3: x = the_Edges_of G0 ;
thus x = the_Edges_of G by A3, TARSKI:def 1; :: thesis: verum

end;

assume A4: x = the_Edges_of G ; :: thesis: x in the_Edges_of {G}
G in {G} by TARSKI:def 1;
hence x in the_Edges_of {G} by A4; :: thesis: verum

end;

hence the_Edges_of {G} = {(the_Edges_of G)} by TARSKI:def 1; :: thesis: ( the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )

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

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

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

assume x in the_Source_of {G} ; :: thesis: x = the_Source_of G
then consider G0 being Element of {G} such that
A5: x = the_Source_of G0 ;
thus x = the_Source_of G by A5, TARSKI:def 1; :: thesis: verum

end;

assume A6: x = the_Source_of G ; :: thesis: x in the_Source_of {G}
G in {G} by TARSKI:def 1;
hence x in the_Source_of {G} by A6; :: thesis: verum

end;

hence the_Source_of {G} = {(the_Source_of G)} by TARSKI:def 1; :: thesis: the_Target_of {G} = {(the_Target_of G)}

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

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

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

assume x in the_Target_of {G} ; :: thesis: x = the_Target_of G
then consider G0 being Element of {G} such that
A7: x = the_Target_of G0 ;
thus x = the_Target_of G by A7, TARSKI:def 1; :: thesis: verum

end;

assume A8: x = the_Target_of G ; :: thesis: x in the_Target_of {G}
G in {G} by TARSKI:def 1;
hence x in the_Target_of {G} by A8; :: thesis: verum

end;

hence the_Target_of {G} = {(the_Target_of G)} by TARSKI:def 1; :: thesis: verum