let G be _Graph; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Vertices_of {G} ; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Edges_of {G} ; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Source_of {G} ; :: thesis:
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:

end;

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

end;

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

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Target_of {G} ; :: thesis:
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:

end;

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

end;

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