set v = the Vertex of G;

defpred S_{1}[ set ] means ex v being Vertex of G st $1 = G .reachableFrom v;

consider IT being Subset-Family of (the_Vertices_of G) such that

A1: for x being set holds

( x in IT iff ( x in bool (the_Vertices_of G) & S_{1}[x] ) )
from SUBSET_1:sch 1();

set x = G .reachableFrom the Vertex of G;

G .reachableFrom the Vertex of G in IT by A1;

then reconsider IT = IT as non empty Subset-Family of (the_Vertices_of G) ;

take IT ; :: thesis: for x being set holds

( x in IT iff ex v being Vertex of G st x = G .reachableFrom v )

thus for x being set holds

( x in IT iff ex v being Vertex of G st x = G .reachableFrom v ) by A1; :: thesis: verum

defpred S

consider IT being Subset-Family of (the_Vertices_of G) such that

A1: for x being set holds

( x in IT iff ( x in bool (the_Vertices_of G) & S

set x = G .reachableFrom the Vertex of G;

G .reachableFrom the Vertex of G in IT by A1;

then reconsider IT = IT as non empty Subset-Family of (the_Vertices_of G) ;

take IT ; :: thesis: for x being set holds

( x in IT iff ex v being Vertex of G st x = G .reachableFrom v )

thus for x being set holds

( x in IT iff ex v being Vertex of G st x = G .reachableFrom v ) by A1; :: thesis: verum