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

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

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

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

end;

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

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

end;

end;