let IT1, IT2 be non empty Subset of (the_Vertices_of G); :: thesis: ( ( for x being object holds

( x in IT1 iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being object holds

( x in IT2 iff ex W being DWalk of G st W is_Walk_from v,x ) ) implies IT1 = IT2 )

assume that

A3: for x being object holds

( x in IT1 iff ex W being directed Walk of G st W is_Walk_from v,x ) and

A4: for x being object holds

( x in IT2 iff ex W being directed Walk of G st W is_Walk_from v,x ) ; :: thesis: IT1 = IT2

( x in IT1 iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being object holds

( x in IT2 iff ex W being DWalk of G st W is_Walk_from v,x ) ) implies IT1 = IT2 )

assume that

A3: for x being object holds

( x in IT1 iff ex W being directed Walk of G st W is_Walk_from v,x ) and

A4: for x being object holds

( x in IT2 iff ex W being directed Walk of G st W is_Walk_from v,x ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds

( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

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

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

then ex W being directed Walk of G st W is_Walk_from v,x by A4;

hence x in IT1 by A3; :: thesis: verum

end;hereby :: thesis: ( x in IT2 implies x in IT1 )

assume
x in IT2
; :: thesis: x in IT1assume
x in IT1
; :: thesis: x in IT2

then ex W being directed Walk of G st W is_Walk_from v,x by A3;

hence x in IT2 by A4; :: thesis: verum

end;then ex W being directed Walk of G st W is_Walk_from v,x by A3;

hence x in IT2 by A4; :: thesis: verum

then ex W being directed Walk of G st W is_Walk_from v,x by A4;

hence x in IT1 by A3; :: thesis: verum