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