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 A1: t in ].r,s.[ ; :: thesis: not t in {r,s}
then A2: r < t by Th4;
t < s by A1, Th4;
hence not t in {r,s} by A2, TARSKI:def 2; :: thesis: verum