let a, b be Real; :: thesis: ( a <= b implies REAL \ ].a,b.[ <> {} )
assume a <= b ; :: thesis: REAL \ ].a,b.[ <> {}
consider c being Real such that
A1: c < a by XREAL_1:2;
A2: not c in ].a,b.[ by A1, XXREAL_1:4;
c in REAL by XREAL_0:def 1;
hence REAL \ ].a,b.[ <> {} by A2, XBOOLE_0:def 5; :: thesis: verum