let G be _Graph; :: thesis: for a, b being Vertex of 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 ; :: 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 (the_Vertices_of G),
for W being Walk of G2 holds not W is_Walk_from b,a

proof

let G2 be removeVertices of (the_Vertices_of G),; :: 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:24;
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