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