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 ;
( 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)
;
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;
verum
end;
hence
((the_Source_of G) ~) * (the_Target_of G) is Relation of (the_Vertices_of G)
by TARSKI:def 3; verum