rng <%a%> c= {a,(0. F_Real)} by Th20;
hence rng <%a%> c= INT by INT_1:def 2; :: according to RELAT_1:def 19 :: thesis: verum