defpred S_{1}[ 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_{1}[x] )
and

A3: for x being set holds

( x in IT2 iff S_{1}[x] )
; :: thesis: IT1 = IT2

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

A3: for x being set holds

( x in IT2 iff S

now :: thesis: for x being object holds

( x in IT1 iff x in IT2 )

hence
IT1 = IT2
by TARSKI:2; :: thesis: verum( x in IT1 iff x in IT2 )

let x be object ; :: thesis: ( x in IT1 iff x in IT2 )

( x in IT1 iff S_{1}[x] )
by A2;

hence ( x in IT1 iff x in IT2 ) by A3; :: thesis: verum

end;( x in IT1 iff S

hence ( x in IT1 iff x in IT2 ) by A3; :: thesis: verum