let n be Nat; :: thesis: ( n in 4k+3_Primes implies n >= 3 )
assume n in 4k+3_Primes ; :: thesis: n >= 3
then consider k being Nat such that
A1: ( n = (4 * k) + 3 & n is prime ) by Def1;
thus n >= 3 by A1, NAT_1:11; :: thesis: verum