let a, b be Real; :: thesis: ( a < b implies [.a,b.] \/ {b} = [.a,b.] )
assume A1: a < b ; :: thesis: [.a,b.] \/ {b} = [.a,b.]
then [.a,b.] = [.a,b.[ \/ {b} by XXREAL_1:129
.= ([.a,b.[ \/ {b}) \/ {b} by XBOOLE_1:6 ;
hence [.a,b.] \/ {b} = [.a,b.] by A1, XXREAL_1:129; :: thesis: verum