let n be Integer; :: thesis: ( n is composite implies 4 <= n )
assume that
A1: 2 <= n and
A2: not n is prime ; :: according to NUMBER02:def 1 :: thesis: 4 <= n
reconsider m = n as Element of NAT by A1, INT_1:3;
assume A3: n < 4 ; :: thesis: contradiction
then not not m = 2 + 0 & ... & not m = 2 + 2 by A1, NAT_1:62;
hence contradiction by A2, A3, INT_2:28, PEPIN:41; :: thesis: verum