let p be ExtReal; :: thesis: for a being Real holds ].-infty,p.[ /\ [.a,+infty.[ = [.a,p.[
let a be Real; :: 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