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:11;
(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:11;
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:16;
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