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

proof

assume p in ].r,r.] ; :: thesis: p in {}
then ex a being Element of ExtREAL st
( p = a & r < a & a <= r ) ;
hence p in {} ; :: thesis: verum

end;

thus ( not p in {} or p in ].r,r.] ) ; :: thesis: verum