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 } ;

then reconsider X = { S where S is VertexSeparator of a,b : verum } as non empty finite set by A1;

defpred S_{1}[ object , object ] means ex p being VertexSeparator of a,b st

( $1 = p & $2 = card p );

A4: for x being object st x in X holds

S_{1}[x,F . x]
from FUNCT_2:sch 1(A2);

deffunc H_{1}( Element of X) -> Element of REAL = F /. $1;

consider Min being Element of X such that

A5: for N being Element of X holds H_{1}(Min) <= H_{1}(N)
from PRE_CIRC:sch 5();

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;

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 (the_Vertices_of G)

then
{ S where S is VertexSeparator of a,b : verum } c= bool (the_Vertices_of G)
;x in bool (the_Vertices_of G)

let x be object ; :: thesis: ( x in { S where S is VertexSeparator of a,b : verum } implies x in bool (the_Vertices_of G) )

assume x in { S where S is VertexSeparator of a,b : verum } ; :: thesis: x in bool (the_Vertices_of G)

then ex y being VertexSeparator of a,b st x = y ;

hence x in bool (the_Vertices_of G) ; :: thesis: verum

end;assume x in { S where S is VertexSeparator of a,b : verum } ; :: thesis: x in bool (the_Vertices_of G)

then ex y being VertexSeparator of a,b st x = y ;

hence x in bool (the_Vertices_of G) ; :: thesis: verum

then reconsider X = { S where S is VertexSeparator of a,b : verum } as non empty finite set by A1;

defpred S

( $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 & S_{1}[x,y] )

consider F being Function of X,REAL such that ex y being object st

( y in REAL & S

let x be object ; :: thesis: ( x in X implies ex y being object st

( y in REAL & S_{1}[x,y] ) )

assume x in X ; :: thesis: ex y being object st

( y in REAL & S_{1}[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 & S_{1}[x,y] )
by A3; :: thesis: verum

end;( y in REAL & S

assume x in X ; :: thesis: ex y being object st

( y in REAL & S

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 & S

A4: for x being object st x in X holds

S

deffunc H

consider Min being Element of X such that

A5: for N being Element of X holds H

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

hence
ex S being VertexSeparator of a,b st S is minimal
; :: thesis: verumassume
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;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