:: deftheorem defines Positives REALALG1:def 20 :
for R being Ring
for Q being Relation of R holds Positives Q = { a where a is Element of R : 0. R <=_ Q,a } ;