for O being Ordering of R st P c= O holds
0. R in O by REALALG1:25;
then 0. R in { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } ;
hence not /\ (P,R) is empty ; :: thesis: verum