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