1260 = 6 * 210 ;
hence 14 * (14 + 1) divides 35 * (35 + 1) ; :: according to NUMBER05:def 2 :: thesis: ( not 14 divides 35 & not 14 + 1 divides 35 & not 14 divides 35 + 1 & not 14 + 1 divides 35 + 1 )
35 = (2 * 14) + 7 ;
hence not 14 divides 35 by NAT_4:9; :: thesis: ( not 14 + 1 divides 35 & not 14 divides 35 + 1 & not 14 + 1 divides 35 + 1 )
35 = (2 * 15) + 5 ;
hence not 14 + 1 divides 35 by NAT_4:9; :: thesis: ( not 14 divides 35 + 1 & not 14 + 1 divides 35 + 1 )
36 = (2 * 14) + 8 ;
hence not 14 divides 35 + 1 by NAT_4:9; :: thesis: not 14 + 1 divides 35 + 1
36 = (2 * 15) + 6 ;
hence not 14 + 1 divides 35 + 1 by NAT_4:9; :: thesis: verum