:: deftheorem defines with_preinterior ROUGHS_4:def 22 :
for X being 2ndOpStr holds
( X is with_preinterior iff the SecondOp of X is preinterior );