take R = {[0,0]}; :: thesis: not R is non-zero
[0,0] in R by TARSKI:def 1;
hence 0 in rng R by XTUPLE_0:def 13; :: according to ORDINAL1:def 15 :: thesis: verum