set Cut = (m,n) -cut F;

set X = rng ((m,n) -cut F);

m < n + 1 by A2, NAT_1:13;

then A4: m - m < (n + 1) - m by XREAL_1:9;

(len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

then A5: not (m,n) -cut F is empty by A4;

rng ((m,n) -cut F) is Subset of INT ;

then reconsider X = rng ((m,n) -cut F) as non empty finite Subset of INT by A5;

set q = (((min X) .. ((m,n) -cut F)) + m) - 1;

1 - 1 <= m - 1 by A1, XREAL_1:9;

then 0 + 0 <= ((min X) .. ((m,n) -cut F)) + (m - 1) ;

then reconsider q = (((min X) .. ((m,n) -cut F)) + m) - 1 as Element of NAT by INT_1:3;

take q ; :: thesis: ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & q + 1 = ((min X) .. ((m,n) -cut F)) + m )

take X ; :: thesis: ( X = rng ((m,n) -cut F) & q + 1 = ((min X) .. ((m,n) -cut F)) + m )

thus X = rng ((m,n) -cut F) ; :: thesis: q + 1 = ((min X) .. ((m,n) -cut F)) + m

thus q + 1 = ((min X) .. ((m,n) -cut F)) + m ; :: thesis: verum

set X = rng ((m,n) -cut F);

m < n + 1 by A2, NAT_1:13;

then A4: m - m < (n + 1) - m by XREAL_1:9;

(len ((m,n) -cut F)) + m = n + 1 by A1, A2, A3, Def1;

then A5: not (m,n) -cut F is empty by A4;

rng ((m,n) -cut F) is Subset of INT ;

then reconsider X = rng ((m,n) -cut F) as non empty finite Subset of INT by A5;

set q = (((min X) .. ((m,n) -cut F)) + m) - 1;

1 - 1 <= m - 1 by A1, XREAL_1:9;

then 0 + 0 <= ((min X) .. ((m,n) -cut F)) + (m - 1) ;

then reconsider q = (((min X) .. ((m,n) -cut F)) + m) - 1 as Element of NAT by INT_1:3;

take q ; :: thesis: ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & q + 1 = ((min X) .. ((m,n) -cut F)) + m )

take X ; :: thesis: ( X = rng ((m,n) -cut F) & q + 1 = ((min X) .. ((m,n) -cut F)) + m )

thus X = rng ((m,n) -cut F) ; :: thesis: q + 1 = ((min X) .. ((m,n) -cut F)) + m

thus q + 1 = ((min X) .. ((m,n) -cut F)) + m ; :: thesis: verum