n in NAT by ORDINAL1:def 13;
then A1: rng (n,(len S) -cut S) c= rng S by GRAPH_2:11;

now

let x be set ; :: 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;

hence S .followSet n is Subset of by TARSKI:def 3; :: thesis: verum