consider v being Vertex of ;
defpred S₁[ set ] means ex v being Vertex of st $1 = G .reachableFrom v;
consider IT being Subset-Family of such that
A1: for x being set holds
( x in IT iff ( x in bool (the_Vertices_of G) & S₁[x] ) ) from SUBSET_1:sch 1();
set x = G .reachableFrom v;
G .reachableFrom v in IT by A1;
then reconsider IT = IT as non empty Subset-Family of ;
take IT ; :: thesis: for x being set holds
( x in IT iff ex v being Vertex of st x = G .reachableFrom v )
thus for x being set holds
( x in IT iff ex v being Vertex of st x = G .reachableFrom v ) by A1; :: thesis: verum