let a, b be Real; ].-infty,a.] \/ {b} <> REAL
set ab = (max (a,b)) + 1;
A1:
(max (a,b)) + 1 > max (a,b)
by XREAL_1:29;
max (a,b) >= a
by XXREAL_0:25;
then
(max (a,b)) + 1 > a
by A1, XXREAL_0:2;
then A2:
not (max (a,b)) + 1 in ].-infty,a.]
by XXREAL_1:234;
max (a,b) >= b
by XXREAL_0:25;
then A3:
not (max (a,b)) + 1 in {b}
by A1, TARSKI:def 1;
(max (a,b)) + 1 in REAL
by XREAL_0:def 1;
hence
].-infty,a.] \/ {b} <> REAL
by A2, A3, XBOOLE_0:def 3; verum