:: deftheorem CDef defines with_closure ROUGHS_4:def 15 :
for X being 1stOpStr holds
( X is with_closure iff the FirstOp of X is closure );