let p be ext-real number ; :: thesis: for a being real number holds ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[
let a be real number ; :: thesis: ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[
a in REAL by XREAL_0:def 1;
then -infty < a by XXREAL_0:12;
hence ].-infty ,p.[ /\ [.a,+infty .[ = [.a,p.[ by Th154, XXREAL_0:3; :: thesis: verum