let a, b be Real; :: thesis: ex c being Real st
( c < a & c < b )

per cases ( a <= b or b <= a ) ;

suppose A1: a <= b ; :: thesis: ex c being Real st
( c < a & c < b )

take z = a + (- 1); :: thesis: ( z < a & z < b )
z < a + 0 by Lm10;
hence ( z < a & z < b ) by A1, XXREAL_0:2; :: thesis: verum

end;

suppose A2: b <= a ; :: thesis: ex c being Real st
( c < a & c < b )

take z = b + (- 1); :: thesis: ( z < a & z < b )
z < b + 0 by Lm10;
hence ( z < a & z < b ) by A2, XXREAL_0:2; :: thesis: verum

end;

end;