let a, b be Real; :: 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, Th10
.= ({a,b} \/ ].a,b.[) \/ [.b,+infty.[ by A2, XXREAL_1:128
.= ({a,b} \/ ].a,b.[) \/ ({b} \/ ].b,+infty.[) by Th42
.= (({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:9
.= {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:51;
hence [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} by ENUMSET1:1; :: thesis: verum