A1: 130 = (2 * 5) * 13 ;
A2: 2,5,13 are_mutually_distinct ;
( 130 = (5 * 13) * 2 & 130 = (13 * 2) * 5 ) ;
then ( 2 divides 130 & 5 divides 130 & 13 divides 130 ) by A1;
hence 131 - 1 is having_at_least_three_different_prime_divisors by A2, XPRIMES1:2, XPRIMES1:5, XPRIMES1:13; :: according to NUMBER08:def 9 :: thesis: 131 + 1 is having_at_least_three_different_prime_divisors
A3: 132 = ((2 * 2) * 3) * 11 ;
A4: 2,3,11 are_mutually_distinct ;
( 132 = ((3 * 11) * 2) * 2 & 132 = ((11 * 2) * 2) * 3 ) ;
then ( 2 divides 132 & 3 divides 132 & 11 divides 132 ) by A3;
hence 131 + 1 is having_at_least_three_different_prime_divisors by A4, XPRIMES1:2, XPRIMES1:3, XPRIMES1:11; :: thesis: verum