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.[ ) )
for p being ExtReal holds not p in [.r,r.[

proof

given p being ExtReal such that A1: p in [.r,r.[ ; :: thesis: contradiction
ex a being Element of ExtREAL st
( p = a & r <= a & a < r ) by A1;
hence contradiction ; :: thesis: verum

end;

hence ( ( not p in [.r,r.[ or p in {} ) & ( not p in {} or p in [.r,r.[ ) ) ; :: thesis: verum