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 st S is minimal holds
for T being VertexSeparator of b,a st S = T holds
T is minimal
let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds
for T being VertexSeparator of b,a st S = T holds
T is minimal )
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds
for T being VertexSeparator of b,a st S = T holds
T is minimal
let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for T being VertexSeparator of b,a st S = T holds
T is minimal )
assume A3: S is minimal ; :: thesis: for T being VertexSeparator of b,a st S = T holds
T is minimal
let T be VertexSeparator of b,a; :: thesis: ( S = T implies T is minimal )
assume A4: S = T ; :: thesis: T is minimal
assume not T is minimal ; :: thesis: contradiction
then consider H being Subset of T such that
A5: H <> T and
A6: H is VertexSeparator of b,a by Def9;
H is VertexSeparator of a,b by A1, A2, A6, Th70;
hence contradiction by A3, A4, A5, Def9; :: thesis: verum