let i1, i2, i3, i4, c be Nat; :: thesis: ( i1 <= c & i2 <= c & i3 <= c & i4 <= c & not ((i1 + i2) + i3) + i4 < 4 * c implies ( i1 = c & i2 = c & i3 = c & i4 = c ) )
assume that
A1: i1 <= c and
A2: i2 <= c and
A3: i3 <= c and
A4: i4 <= c ; :: thesis: ( ((i1 + i2) + i3) + i4 < 4 * c or ( i1 = c & i2 = c & i3 = c & i4 = c ) )

per cases ( ( i1 + i2 < 2 * c & i3 + i4 < 2 * c ) or ( i1 + i2 < 2 * c & i3 = c & i4 = c ) or ( i1 = c & i2 = c & i3 + i4 < 2 * c ) or ( i1 = c & i2 = c & i3 = c & i4 = c ) ) by A1, A2, A3, A4, lem7;

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

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

end;

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

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

end;

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

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

end;

suppose ( i1 = c & i2 = c & i3 = c & i4 = c ) ; :: thesis: ( ((i1 + i2) + i3) + i4 < 4 * c or ( i1 = c & i2 = c & i3 = c & i4 = c ) )

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

end;

end;