reconsider z = 0 , j = 1 as Element of REAL+ by ARYTM_2:20;
z <=' j by ARYTM_1:6;
hence 0 <= 1 by Lm2; :: thesis: verum