let x be set ; :: thesis: for p, q being ExtReal st x in ].p,q.] holds
( x in [.p,q.] & x <> p )
let p, q be ExtReal; :: 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 ExtReal ;
A2: p < s by A1, Th2;
s <= q by A1, Th2;
hence ( x in [.p,q.] & x <> p ) by A2, Th1; :: thesis: verum