let n be Nat; :: thesis: ( 5 <= n implies card (primeNumbers (n,21)) <= 7 )
assume A1: 5 <= n ; :: thesis: card (primeNumbers (n,21)) <= 7
set M2 = multiples 2;
set M3 = multiples 3;
set M5 = multiples 5;
set M = ((multiples 2) \/ (multiples 3)) \/ (multiples 5);
set S = seq (n,21);
A2: primeNumbers (n,21) misses (seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))

proof

assume primeNumbers (n,21) meets (seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ; :: thesis: contradiction
then consider x being object such that
A3: ( x in primeNumbers (n,21) & x in (seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ) by XBOOLE_0:3;
reconsider x = x as Nat by A3;
A4: ( x is prime & n < x ) by A3, Th74;
( 2 divides x or 3 divides x or 5 divides x ) by A3, Lm6;
then ( x = 2 or x = 3 or x = 5 ) by A4;
hence contradiction by A3, Th74, A1, XXREAL_0:2; :: thesis: verum

end;

primeNumbers (n,21) = (seq (n,21)) /\ SetPrimes by NUMBER14:def 17;
then ( card ((primeNumbers (n,21)) \/ ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) <= card (seq (n,21)) & card (seq (n,21)) = 21 ) by NAT_1:43, NUMBER14:73, XBOOLE_1:8;
then A5: (card (primeNumbers (n,21))) + (card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) <= 21 by A2, CARD_2:40;
set nm = n mod 30;
set nd = n div 30;
A6: n = ((n div 30) * 30) + (n mod 30) by INT_1:59;
( 2 divides 2 * (3 * 5) & 3 divides 3 * (2 * 5) & 5 divides 5 * (2 * 3) ) ;
then A7: ( 2 divides (n div 30) * 30 & 3 divides (n div 30) * 30 & 5 divides (n div 30) * 30 ) by INT_2:2;
((multiples 2) \/ (multiples 3)) \/ (multiples 5) = (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 5) by XBOOLE_1:6
.= ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 5)) \/ (multiples 5) by XBOOLE_1:6 ;
then A8: card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = card ((seq ((n mod 30),21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) by A6, A7, Th88;
n mod 30 < 30 by INT_1:58;
then card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 14 by A8, Th97;
then ((card (primeNumbers (n,21))) + (card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))))) - (card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) <= 21 - 14 by A5, XREAL_1:13;
hence card (primeNumbers (n,21)) <= 7 ; :: thesis: verum