:: deftheorem defppc defines prepositive_cone REALALG1:def 14 :
for R being Ring
for S being Subset of R holds
( S is prepositive_cone iff ( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & SQ R c= S ) );