:: deftheorem defines prime RING_1:def 2 :
for K being non empty multLoopStr
for S being Subset of K holds
( S is prime iff ( S is proper & S is quasi-prime ) );