reconsider S = the_Source_of G as Relation ;
set T = the_Target_of G;
set E = the_Edges_of G;
set V = the_Vertices_of G;
for x being object st x in (S ~) * (the_Target_of G) holds
x in [:(the_Vertices_of G),(the_Vertices_of G):]

proof

let x be object ; :: thesis: ( x in (S ~) * (the_Target_of G) implies x in [:(the_Vertices_of G),(the_Vertices_of G):] )
assume A1: x in (S ~) * (the_Target_of G) ; :: thesis: x in [:(the_Vertices_of G),(the_Vertices_of G):]
then consider y, z being object such that
A2: x = [y,z] by RELAT_1:def 1;
consider a being object such that
A3: ( [y,a] in S ~ & [a,z] in the_Target_of G ) by A1, A2, RELAT_1:def 8;
[a,y] in S by A3, RELAT_1:def 7;
then A4: y in the_Vertices_of G by ZFMISC_1:87;
z in the_Vertices_of G by A3, ZFMISC_1:87;
hence x in [:(the_Vertices_of G),(the_Vertices_of G):] by A2, A4, ZFMISC_1:def 2; :: thesis: verum

end;

hence ((the_Source_of G) ~) * (the_Target_of G) is Relation of (the_Vertices_of G) by TARSKI:def 3; :: thesis: verum