let b be Element of ExtREAL ; :: thesis: for a being real number holds ].-infty ,b.[ /\ [.a,+infty .[ = [.a,b.[
let a be real number ; :: thesis: ].-infty ,b.[ /\ [.a,+infty .[ = [.a,b.[
a in REAL by XREAL_0:def 1;
then ( -infty < a & b <= +infty ) by XXREAL_0:3, XXREAL_0:12;
hence ].-infty ,b.[ /\ [.a,+infty .[ = [.a,b.[ by Th154; :: thesis: verum