let a, b be ext-real number ; :: thesis: ].-infty ,b.[ /\ ].a,+infty .[ = ].a,b.[
( -infty <= a & b <= +infty ) by XXREAL_0:3, XXREAL_0:5;
hence ].-infty ,b.[ /\ ].a,+infty .[ = ].a,b.[ by Th160; :: thesis: verum