let A, B be non empty Interval; :: thesis: for a, b being real number st a in A & b in B & sup A <= inf B holds
a <= b
let a, b be real number ; :: thesis: ( a in A & b in B & sup A <= inf B implies a <= b )
assume A1: ( a in A & b in B ) ; :: thesis: ( not sup A <= inf B or a <= b )
assume A2: sup A <= inf B ; :: thesis: a <= b
( inf A <= R_EAL a & R_EAL a <= sup A & inf B <= R_EAL b & R_EAL b <= sup B ) by A1, XXREAL_2:3, XXREAL_2:4;
then A3: ( R_EAL a <= inf B & inf B <= R_EAL b ) by A2, XXREAL_0:2;
thus a <= b by A3, XXREAL_0:2; :: thesis: verum