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