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