let n be natural number ; :: thesis: ( 1 < n implies 1. (INT.Ring n) = 1 )
assume 1 < n ; :: thesis: 1. (INT.Ring n) = 1
then 1 in Segm n by NAT_1:45;
hence 1. (INT.Ring n) = 1 by FUNCT_7:def 1; :: thesis: verum