let a, b be Real; :: thesis: [.a,+infty.[ \/ {b} <> REAL
set ab = (min (a,b)) - 1;
A1: (min (a,b)) - 1 < min (a,b) by XREAL_1:146;
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:146, 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