let n be Nat; :: thesis: ( n > 15 implies ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes ) )
assume A1: n > 15 ; :: thesis: ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes )

per cases ( n <= 29 or n > 29 ) ;

suppose n <= 29 ; :: thesis: ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes )

then A2: not not n = 0 & ... & not n = 29 ;
take (p2 * p3) * p5 ; :: thesis: ( n < (p2 * p3) * p5 & (p2 * p3) * p5 < 2 * n & (p2 * p3) * p5 is a_product_of_three_different_primes )
thus ( n < (p2 * p3) * p5 & (p2 * p3) * p5 < 2 * n ) by A1, A2; :: thesis: (p2 * p3) * p5 is a_product_of_three_different_primes
take p2 ; :: according to NUMBER10:def 6 :: thesis: ex q, r being Prime st
( p2,q,r are_mutually_distinct & (p2 * p3) * p5 = (p2 * q) * r )
take p3 ; :: thesis: ex r being Prime st
( p2,p3,r are_mutually_distinct & (p2 * p3) * p5 = (p2 * p3) * r )
take p5 ; :: thesis: ( p2,p3,p5 are_mutually_distinct & (p2 * p3) * p5 = (p2 * p3) * p5 )
thus ( p2,p3,p5 are_mutually_distinct & (p2 * p3) * p5 = (p2 * p3) * p5 ) ; :: thesis: verum

end;

suppose A3: n > 29 ; :: thesis: ex m being Nat st
( n < m & m < 2 * n & m is a_product_of_three_different_primes )

consider k being Nat such that
A4: ( n = 6 * k or n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) by NUMBER02:26;
reconsider k = k as Element of NAT by ORDINAL1:def 12;

A5: now :: thesis: not k < 4 + 1

assume k < 4 + 1 ; :: thesis: contradiction
then k <= 4 by NAT_1:13;
then A6: 6 * k <= 6 * 4 by XREAL_1:64;
then ( (6 * k) + 1 <= (6 * 4) + 1 & (6 * k) + 2 <= (6 * 4) + 2 & (6 * k) + 3 <= (6 * 4) + 3 & (6 * k) + 4 <= (6 * 4) + 4 & (6 * k) + 5 <= (6 * 4) + 5 ) by XREAL_1:6;
hence contradiction by A3, A4, A6, XXREAL_0:2; :: thesis: verum

end;

then consider P being Prime such that
A7: k < P and
A8: P <= 2 * k by NAT_4:56, XXREAL_0:2;
take (p2 * p3) * P ; :: thesis: ( n < (p2 * p3) * P & (p2 * p3) * P < 2 * n & (p2 * p3) * P is a_product_of_three_different_primes )
2 <= k by A5, XXREAL_0:2;
then 2 * k is composite by Th3;
then A9: P < 2 * k by A8, XXREAL_0:1;
A10: ( (6 * k) + 0 < (6 * k) + 6 & (6 * k) + 1 < (6 * k) + 6 & (6 * k) + 2 < (6 * k) + 6 & (6 * k) + 3 < (6 * k) + 6 & (6 * k) + 4 < (6 * k) + 6 & (6 * k) + 5 < (6 * k) + 6 ) by XREAL_1:6;
k + 1 <= P by A7, NAT_1:13;
then ( 6 * (k + 1) <= 6 * P & 6 * (k + 1) <= 6 * P & 6 * (k + 1) <= 6 * P & 6 * (k + 1) <= 6 * P & 6 * (k + 1) <= 6 * P & 6 * (k + 1) <= 6 * P ) by XREAL_1:64;
hence n < (p2 * p3) * P by A4, A10, XXREAL_0:2; :: thesis: ( (p2 * p3) * P < 2 * n & (p2 * p3) * P is a_product_of_three_different_primes )
A11: 6 * P < 6 * (2 * k) by A9, XREAL_1:68;
( (12 * k) + 0 <= (12 * k) + 2 & (12 * k) + 0 <= (12 * k) + 4 & (12 * k) + 0 <= (12 * k) + 6 & (12 * k) + 0 <= (12 * k) + 8 & (12 * k) + 0 <= (12 * k) + 10 ) by XREAL_1:6;
hence (p2 * p3) * P < 2 * n by A4, A11, XXREAL_0:2; :: thesis: (p2 * p3) * P is a_product_of_three_different_primes
take p2 ; :: according to NUMBER10:def 6 :: thesis: ex q, r being Prime st
( p2,q,r are_mutually_distinct & (p2 * p3) * P = (p2 * q) * r )
take p3 ; :: thesis: ex r being Prime st
( p2,p3,r are_mutually_distinct & (p2 * p3) * P = (p2 * p3) * r )
take P ; :: thesis: ( p2,p3,P are_mutually_distinct & (p2 * p3) * P = (p2 * p3) * P )
thus ( p2,p3,P are_mutually_distinct & (p2 * p3) * P = (p2 * p3) * P ) by A5, A7, XXREAL_0:2; :: thesis: verum

end;

end;