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