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

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;

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