let r, s be ext-real number ; :: thesis: ].r,s.[ misses {r,s}
let t be ext-real number ; :: according to MEMBERED:def 20 :: thesis: ( not t in ].r,s.[ or not t in {r,s} )
assume t in ].r,s.[ ; :: thesis: not t in {r,s}
then ( r < t & t < s ) by Th4;
hence not t in {r,s} by TARSKI:def 2; :: thesis: verum