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