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;