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
; 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
; ( X = rng ((m,n) -cut F) & q + 1 = ((min X) .. ((m,n) -cut F)) + m )
thus
X = rng ((m,n) -cut F)
; q + 1 = ((min X) .. ((m,n) -cut F)) + m
thus
q + 1 = ((min X) .. ((m,n) -cut F)) + m
; verum