let x be set ; :: thesis: for p, q being ext-real number holds
( not x in [.p,q.[ or x in ].p,q.[ or x = p )
let p, q be ext-real number ; :: thesis: ( not x in [.p,q.[ or x in ].p,q.[ or x = p )
assume A1: x in [.p,q.[ ; :: thesis: ( x in ].p,q.[ or x = p )
then reconsider s = x as ext-real number ;
A2: ( p <= s & s < q ) by A1, Th3;
then ( p = s or p < s ) by XXREAL_0:1;
hence ( x in ].p,q.[ or x = p ) by A2, Th4; :: thesis: verum