:: deftheorem defines op-closed ROUGHS_4:def 17 :
for X being 1stOpStr
for A being Subset of X holds
( A is op-closed iff A = the FirstOp of X . A );