0. R <= P, 0. R by ord3;
then [(0. R),(0. R)] in { [a,b] where a, b is Element of R : a <= P,b } ;
hence not OrdRel P is empty ; :: thesis: verum