take 1. R ; :: thesis: 1. R is P -ordered
1. R in P by REALALG1:25;
hence 1. R is P -ordered by XBOOLE_0:def 3; :: thesis: verum