let G be finite _Graph; :: thesis: for a, b being Vertex of G ex S being VertexSeparator of a,b st S is minimal
let a, b be Vertex of G; :: thesis: ex S being VertexSeparator of a,b st S is minimal
set X = { S where S is VertexSeparator of a,b : verum } ;
set s = the VertexSeparator of a,b;
A1: the VertexSeparator of a,b in { S where S is VertexSeparator of a,b : verum } ;
now :: thesis: for x being object st x in { S where S is VertexSeparator of a,b : verum } holds
x in bool ()
let x be object ; :: thesis: ( x in { S where S is VertexSeparator of a,b : verum } implies x in bool () )
assume x in { S where S is VertexSeparator of a,b : verum } ; :: thesis:
then ex y being VertexSeparator of a,b st x = y ;
hence x in bool () ; :: thesis: verum
end;
then { S where S is VertexSeparator of a,b : verum } c= bool () ;
then reconsider X = { S where S is VertexSeparator of a,b : verum } as non empty finite set by A1;
defpred S1[ object , object ] means ex p being VertexSeparator of a,b st
( \$1 = p & \$2 = card p );
A2: now :: thesis: for x being object st x in X holds
ex y being object st
( y in REAL & S1[x,y] )
let x be object ; :: thesis: ( x in X implies ex y being object st
( y in REAL & S1[x,y] ) )

assume x in X ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

then consider Y being VertexSeparator of a,b such that
A3: Y = x ;
card Y in REAL by NUMBERS:19;
hence ex y being object st
( y in REAL & S1[x,y] ) by A3; :: thesis: verum
end;
consider F being Function of X,REAL such that
A4: for x being object st x in X holds
S1[x,F . x] from deffunc H1( Element of X) -> Element of REAL = F /. \$1;
consider Min being Element of X such that
A5: for N being Element of X holds H1(Min) <= H1(N) from consider M being VertexSeparator of a,b such that
M = Min and
A6: card M = F . Min by A4;
A7: dom F = X by FUNCT_2:def 1;
now :: thesis: M is minimal
assume not M is minimal ; :: thesis: contradiction
then consider T being Subset of M such that
A8: T <> M and
A9: T is VertexSeparator of a,b ;
T in X by A9;
then reconsider T2 = T as Element of X ;
consider Tp being VertexSeparator of a,b such that
A10: Tp = T2 and
A11: card Tp = F . T2 by A4;
Tp in dom F by A7;
then F /. Tp = F . Tp by PARTFUN1:def 6;
then A12: card M <= card T by A5, A6, A10, A11;
card T <= card M by NAT_1:43;
hence contradiction by A8, A12, CARD_2:102, XXREAL_0:1; :: thesis: verum
end;
hence ex S being VertexSeparator of a,b st S is minimal ; :: thesis: verum