let n be Nat; :: thesis: ( n > 0 & n is having_at_least_three_different_prime_divisors implies n >= 30 )
assume A1: n > 0 ; :: thesis: ( not n is having_at_least_three_different_prime_divisors or n >= 30 )
given p1, p2, p3 being Prime such that A2: p1,p2,p3 are_mutually_distinct and
A3: ( p1 divides n & p2 divides n & p3 divides n ) ; :: according to NUMBER08:def 8 :: thesis: n >= 30
( ( p1 >= 2 & p2 >= 3 & p3 >= 5 ) or ( p1 >= 2 & p2 >= 5 & p3 >= 3 ) or ( p1 >= 3 & p2 >= 2 & p3 >= 5 ) or ( p1 >= 3 & p2 >= 5 & p3 >= 2 ) or ( p1 >= 5 & p2 >= 2 & p3 >= 3 ) or ( p1 >= 5 & p2 >= 3 & p3 >= 2 ) ) by A2, Th49;
then A4: ( (p1 * p2) * p3 >= (2 * 3) * 5 or (p1 * p2) * p3 >= (3 * 5) * 2 or (p1 * p2) * p3 >= (5 * 2) * 3 ) by Lm15;
A5: p1 * p2 divides n by A2, A3, PEPIN:4, INT_2:30;
( p1,p3 are_coprime & p2,p3 are_coprime ) by A2, INT_2:30;
then p1 * p2,p3 are_coprime by EULER_1:14;
then (p1 * p2) * p3 <= n by A1, A3, A5, NAT_D:7, PEPIN:4;
hence n >= 30 by A4, XXREAL_0:2; :: thesis: verum