set v = the Vertex of G;
defpred S₁[ 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₁[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