defpred S₁[ object ] means ex v being Vertex of G st $1 = G .reachableFrom v;
let IT1, IT2 be non empty Subset-Family of (the_Vertices_of G); :: thesis: ( ( for x being set holds
( x in IT1 iff ex v being Vertex of G st x = G .reachableFrom v ) ) & ( for x being set holds
( x in IT2 iff ex v being Vertex of G st x = G .reachableFrom v ) ) implies IT1 = IT2 )
assume that
A2: for x being set holds
( x in IT1 iff S₁[x] ) and
A3: for x being set holds
( x in IT2 iff S₁[x] ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds
( x in IT1 iff x in IT2 )

let x be object ; :: thesis: ( x in IT1 iff x in IT2 )
( x in IT1 iff S₁[x] ) by A2;
hence ( x in IT1 iff x in IT2 ) by A3; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum