:: deftheorem defines with_interior ROUGHS_4:def 21 :
for X being 2ndOpStr holds
( X is with_interior iff the SecondOp of X is interior );