defpred S1[ 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 S1[x] ) and
A3: for x being set holds
( x in IT2 iff S1[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 S1[x] ) by A2;
hence ( x in IT1 iff x in IT2 ) by A3; :: thesis: verum
end;
hence IT1 = IT2 by TARSKI:2; :: thesis: verum