theorem :: REALALG2:22

for P being Preordering of F_Real holds P = Positives(F_Real) by REALALG1:36;