let k be Nat; :: thesis: for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
let a, b, c be Element of NAT ; :: thesis: ( 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k implies k = a - 1 )
assume that
A1: 1 <= a and
A2: 2 <= b and
A3: a - 1 <= k and
A4: ( a > k or k > (a + b) - 3 ) and
A5: k <> (a + b) - 2 and
A6: k <= (a + b) - 2 ; :: thesis: k = a - 1
A7: a - 1 is Element of NAT by A1, INT_1:5;
now :: thesis: ( ( k < a & k <= a - 1 ) or ( (a + b) - 3 < k & k <= a - 1 ) )
per cases ( k < a or (a + b) - 3 < k ) by A4;
case k < a ; :: thesis: k <= a - 1
then k < (a - 1) + 1 ;
hence k <= a - 1 by A7, NAT_1:13; :: thesis: verum
end;
case A8: (a + b) - 3 < k ; :: thesis: k <= a - 1
1 + 2 <= a + b by A1, A2, XREAL_1:7;
then A9: (a + b) - 3 is Element of NAT by INT_1:5;
k < ((a + b) - 3) + 1 by A5, A6, XXREAL_0:1;
hence k <= a - 1 by A8, A9, NAT_1:13; :: thesis: verum
end;
end;
end;
hence k = a - 1 by A3, XXREAL_0:1; :: thesis: verum