let i1, i2, c be Nat; :: thesis: ( i1 <= c & i2 <= c & not i1 + i2 < 2 * c implies ( i1 = c & i2 = c ) )
assume that
A1: i1 <= c and
A2: i2 <= c ; :: thesis: ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) )
i1 in [.0,c.] by A1, XXREAL_1:1;
then A3: ( i1 in [.0,c.[ or i1 = c ) by XXREAL_1:7;
i2 in [.0,c.] by A2, XXREAL_1:1;
then A4: ( i2 in [.0,c.[ or i2 = c ) by XXREAL_1:7;

per cases ( ( i1 = c & i2 = c ) or ( 0 <= i1 & i1 < c & 0 <= i2 & i2 < c ) or ( 0 <= i1 & i1 < c & i2 = c ) or ( 0 <= i2 & i2 < c & i1 = c ) ) by A3, XXREAL_1:3, A4;

suppose ( i1 = c & i2 = c ) ; :: thesis: ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) )

hence ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) ) ; :: thesis: verum

end;

suppose ( 0 <= i1 & i1 < c & 0 <= i2 & i2 < c ) ; :: thesis: ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) )

then i1 + i2 < c + c by XREAL_1:8;
hence ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) ) ; :: thesis: verum

end;

suppose ( 0 <= i1 & i1 < c & i2 = c ) ; :: thesis: ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) )

then i1 + i2 < c + c by XREAL_1:8;
hence ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) ) ; :: thesis: verum

end;

suppose ( 0 <= i2 & i2 < c & i1 = c ) ; :: thesis: ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) )

then i1 + i2 < c + c by XREAL_1:8;
hence ( i1 + i2 < 2 * c or ( i1 = c & i2 = c ) ) ; :: thesis: verum

end;

end;