let x be set ; for p, q being ExtReal st x in [.p,q.[ holds
( x in [.p,q.] & x <> q )
let p, q be ExtReal; ( x in [.p,q.[ implies ( x in [.p,q.] & x <> q ) )
assume A1:
x in [.p,q.[
; ( x in [.p,q.] & x <> q )
then reconsider s = x as ExtReal ;
A2:
p <= s
by A1, Th3;
s < q
by A1, Th3;
hence
( x in [.p,q.] & x <> q )
by A2, Th1; verum