let p, r, s be ExtReal; :: thesis: ( r < s implies [.s,p.[ c= ].r,p.[ )
assume A1: r < s ; :: thesis: [.s,p.[ c= ].r,p.[
let t be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not t in [.s,p.[ or t in ].r,p.[ )
assume A2: t in [.s,p.[ ; :: thesis: t in ].r,p.[
then s <= t by Th3;
then A3: r < t by A1, XXREAL_0:2;
t < p by A2, Th3;
hence t in ].r,p.[ by A3, Th4; :: thesis: verum