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