A1:
rng ((n,(len S)) -cut S) c= rng S
by FINSEQ_6:137;

now :: thesis: for x being object st x in S .followSet n holds

x in the_Vertices_of G

hence
S .followSet n is Subset of (the_Vertices_of G)
by TARSKI:def 3; :: thesis: verumx in the_Vertices_of G

let x be object ; :: thesis: ( x in S .followSet n implies x in the_Vertices_of G )

assume x in S .followSet n ; :: thesis: x in the_Vertices_of G

then x in rng S by A1;

hence x in the_Vertices_of G by Def12; :: thesis: verum

end;assume x in S .followSet n ; :: thesis: x in the_Vertices_of G

then x in rng S by A1;

hence x in the_Vertices_of G by Def12; :: thesis: verum