theorem lemPP: :: REALALG3:8

for F being ordered Field
for P being Ordering of F
for E being Field st E == F holds
( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) )