:: deftheorem defines with_preclosure ROUGHS_4:def 16 :
for X being 1stOpStr holds
( X is with_preclosure iff the FirstOp of X is preclosure );