let r, s be ExtReal; :: thesis: ].r,s.] misses {r}
let t be ExtReal; :: according to MEMBERED:def 20 :: thesis: ( not t in ].r,s.] or not t in {r} )
assume t in ].r,s.] ; :: thesis: not t in {r}
then r < t by Th2;
hence not t in {r} by TARSKI:def 1; :: thesis: verum