:: deftheorem OOS defines with_op-open_subsets ROUGHS_4:def 20 :
for X being 2ndOpStr holds
( X is with_op-open_subsets iff ex A being Subset of X st A is op-open );