:: deftheorem OCS defines with_op-closed_subsets ROUGHS_4:def 18 :
for X being 1stOpStr holds
( X is with_op-closed_subsets iff ex A being Subset of X st A is op-closed );