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