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