0. R <=_ Q, 0. R by defstr, RELAT_2:def 1;
then 0. R in Positives Q ;
hence not Positives Q is empty ; :: thesis: verum