let G be _Graph; :: thesis: for W1, W2 being Walk of G
for x, y being set st W1 is Subwalk of W2 holds
( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
let W1, W2 be Walk of G; :: thesis: for x, y being set st W1 is Subwalk of W2 holds
( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
let x, y be set ; :: thesis: ( W1 is Subwalk of W2 implies ( W1 is_Walk_from x,y iff W2 is_Walk_from x,y ) )
assume A1: W1 is Subwalk of W2 ; :: thesis: ( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
hereby :: thesis: ( W2 is_Walk_from x,y implies W1 is_Walk_from x,y )
A2: W1 is_Walk_from W2 .first() ,W2 .last() by A1, Def32;
assume A3: W1 is_Walk_from x,y ; :: thesis: W2 is_Walk_from x,y
then W1 .last() = y ;
then A4: y = W2 .last() by A2;
W1 .first() = x by A3;
then x = W2 .first() by A2;
hence W2 is_Walk_from x,y by A4; :: thesis: verum
end;
assume A5: W2 is_Walk_from x,y ; :: thesis: W1 is_Walk_from x,y
then A6: W2 .last() = y ;
W2 .first() = x by A5;
hence W1 is_Walk_from x,y by A1, A6, Def32; :: thesis: verum