let G be _Graph; :: thesis: for a, b being Vertex of G
for S being VertexSeparator of a,b st S = {} holds
S is minimal
let a, b be Vertex of G; :: thesis: for S being VertexSeparator of a,b st S = {} holds
S is minimal
let S be VertexSeparator of a,b; :: thesis: ( S = {} implies S is minimal )
assume A1: S = {} ; :: thesis: S is minimal

now

assume not S is minimal ; :: thesis: contradiction
then ex T being Subset of S st
( T <> S & T is VertexSeparator of a,b ) by Def9;
hence contradiction by A1; :: thesis: verum

end;

hence S is minimal ; :: thesis: verum