let G be _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b holds S is VertexSeparator of b,a
let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b holds S is VertexSeparator of b,a )
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b holds S is VertexSeparator of b,a
let S be VertexSeparator of a,b; :: thesis: S is VertexSeparator of b,a
A3: not b in S by A1, A2, Def8;
A4: for G2 being removeVertices of G,S
for W being Walk of G2 holds not W is_Walk_from b,a

proof

let G2 be removeVertices of G,S; :: thesis: for W being Walk of G2 holds not W is_Walk_from b,a
let W be Walk of G2; :: thesis: not W is_Walk_from b,a
assume W is_Walk_from b,a ; :: thesis: contradiction
then W .reverse() is_Walk_from a,b by GLIB_001:23;
hence contradiction by A1, A2, Def8; :: thesis: verum

end;

not a in S by A1, A2, Def8;
hence S is VertexSeparator of b,a by A1, A2, A3, A4, Def8; :: thesis: verum