:: deftheorem defines preclosure ROUGHS_4:def 11 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is preclosure iff ( O is extensive & O is \/-preserving & O is empty-preserving ) );