let n be Nat; :: thesis:
assume n > 4 ; :: thesis:
then consider k being Nat such that
A1: ( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) ) by Th37;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider p2 = 2 as Prime by XPRIMES1:2;

per cases by A1;

suppose that A2: n = 2 * k and
A3: k > 2 ; :: thesis:

consider P being Prime such that
A4: k < P and
A5: P <= 2 * k by A3, XXREAL_0:2, NAT_4:56;
take m = p2 * P; :: thesis:
thus n < m by A2, A4, XREAL_1:68; :: thesis:
2 * k is composite by A3, Th3;
then P < n by A2, A5, XXREAL_0:1;
hence m < 2 * n by XREAL_1:68; :: thesis:
take p2 ; :: according to NUMBER07:def 5 :: thesis:
take P ; :: thesis:
thus p2 <> P by A3, A4; :: thesis:
thus m = p2 * P ; :: thesis:

end;

suppose that A6: n = (2 * k) + 1 and
A7: k > 1 ; :: thesis:

consider P being Prime such that
A8: k < P and
A9: P <= 2 * k by A7, NAT_4:56;
take m = p2 * P; :: thesis:
k + 1 <= P by A8, NAT_1:13;
then A10: 2 * (k + 1) <= 2 * P by XREAL_1:64;
(2 * k) + 1 < (2 * k) + 2 by XREAL_1:6;
hence n < m by A6, A10, XXREAL_0:2; :: thesis:
A11: 2 * P <= 2 * (2 * k) by A9, XREAL_1:64;
(4 * k) + 0 < (4 * k) + 2 by XREAL_1:6;
hence m < 2 * n by A6, A11, XXREAL_0:2; :: thesis:
take p2 ; :: according to NUMBER07:def 5 :: thesis:
take P ; :: thesis:
k >= 1 + 1 by A7, NAT_1:13;
hence p2 <> P by A8; :: thesis:
thus m = p2 * P ; :: thesis:
thus verum ; :: thesis:

end;

end;