let r be ExtReal; :: thesis: [.r,r.] = {r}
let s be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not s in [.r,r.] or s in {r} ) & ( not s in {r} or s in [.r,r.] ) )
thus ( s in [.r,r.] implies s in {r} ) :: thesis: ( not s in {r} or s in [.r,r.] )

proof

assume s in [.r,r.] ; :: thesis: s in {r}
then ex a being Element of ExtREAL st
( s = a & r <= a & a <= r ) ;
then s = r by XXREAL_0:1;
hence s in {r} by TARSKI:def 1; :: thesis: verum

end;

assume s in {r} ; :: thesis: s in [.r,r.]
then A1: s = r by TARSKI:def 1;
reconsider s = s as Element of ExtREAL by XXREAL_0:def 1;
s <= s ;
hence s in [.r,r.] by A1; :: thesis: verum