:: deftheorem defines op-open ROUGHS_4:def 19 :
for X being 2ndOpStr
for A being Subset of X holds
( A is op-open iff A = the SecondOp of X . A );