:: deftheorem defines interior ROUGHS_4:def 14 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is interior iff ( O is intensive & O is idempotent & O is /\-preserving & O is universe-preserving ) );