:: deftheorem defines primary IDEAL_2:def 5 :
for A being non empty well-unital doubleLoopStr
for S being Subset of A holds
( S is primary iff ( S is proper & S is quasi-primary ) );