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