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

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

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

not a in S
by A1, A2, Def8;
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;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

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