:: deftheorem Def5 defines open RCOMP_1:def 5 :
for X being Subset of REAL holds
( X is open iff X ` is closed );