let a, b be real number ; :: thesis: ( a < b implies [.a,+infty .[ \ (].a,b.[ \/ ].b,+infty .[) = {a} \/ {b} )
A1: not b in ].a,b.[ \/ ].b,+infty .[ by XXREAL_1:205;
assume A2: a < b ; :: thesis: [.a,+infty .[ \ (].a,b.[ \/ ].b,+infty .[) = {a} \/ {b}
then A3: not a in ].a,b.[ \/ ].b,+infty .[ by XXREAL_1:223;
[.a,+infty .[ = [.a,b.] \/ [.b,+infty .[ by A2, Th28
.= ({a,b} \/ ].a,b.[) \/ [.b,+infty .[ by A2, XXREAL_1:128
.= ({a,b} \/ ].a,b.[) \/ ({b} \/ ].b,+infty .[) by Th67
.= (({a,b} \/ ].a,b.[) \/ {b}) \/ ].b,+infty .[ by XBOOLE_1:4
.= (({a,b} \/ {b}) \/ ].a,b.[) \/ ].b,+infty .[ by XBOOLE_1:4
.= ({a,b} \/ ].a,b.[) \/ ].b,+infty .[ by ZFMISC_1:14
.= {a,b} \/ (].a,b.[ \/ ].b,+infty .[) by XBOOLE_1:4 ;
then [.a,+infty .[ \ (].a,b.[ \/ ].b,+infty .[) = {a,b} by A3, A1, XBOOLE_1:88, ZFMISC_1:57;
hence [.a,+infty .[ \ (].a,b.[ \/ ].b,+infty .[) = {a} \/ {b} by ENUMSET1:41; :: thesis: verum