:: deftheorem defpc defines positive_cone REALALG1:def 15 :
for R being Ring
for S being Subset of R holds
( S is positive_cone iff ( S + S c= S & S * S c= S & S /\ (- S) = {(0. R)} & S \/ (- S) = the carrier of R ) );