let a, b be real number ; ].-infty ,a.] \/ {b} <> REAL
set ab = (max a,b) + 1;
A1:
(max a,b) + 1 > max a,b
by XREAL_1:31;
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