let k be Nat; :: thesis: ( 2 <= k implies card (primeNumbers (k,10)) <= 4 )
set A = primeNumbers (k,10);
assume 2 <= k ; :: thesis: card (primeNumbers (k,10)) <= 4

per cases then ( k = 2 or k > 2 ) by XXREAL_0:1;

suppose k = 2 ; :: thesis: card (primeNumbers (k,10)) <= 4

hence card (primeNumbers (k,10)) <= 4 by Th71, CARD_2:59; :: thesis: verum

end;

suppose A1: k > 2 ; :: thesis: card (primeNumbers (k,10)) <= 4

consider m being Multiple of 3 such that
A2: m in seq (k,10) and
A3: m is odd by Th84;
set D = (multiples 2) /\ (seq (k,10));

A4: now :: thesis: not m in (multiples 2) /\ (seq (k,10))

assume m in (multiples 2) /\ (seq (k,10)) ; :: thesis: contradiction
then reconsider m = m as Multiple of 2 by Th61;
2 divides m by Def15;
hence contradiction by A3; :: thesis: verum

end;

set W = ((multiples 2) /\ (seq (k,10))) \/ {m};
10 = 2 * 5 ;
then card ((multiples 2) /\ (seq (k,10))) = 5 by Th83;
then A5: card (((multiples 2) /\ (seq (k,10))) \/ {m}) = 5 + 1 by A4, CARD_2:41;
A6: card (seq (k,10)) = 10 by Th73;
A7: k + 1 > 2 + 1 by A1, XREAL_1:6;

now :: thesis: not ((multiples 2) /\ (seq (k,10))) \/ {m} meets primeNumbers (k,10)

assume ((multiples 2) /\ (seq (k,10))) \/ {m} meets primeNumbers (k,10) ; :: thesis: contradiction
then consider x being object such that
A8: x in ((multiples 2) /\ (seq (k,10))) \/ {m} and
A9: x in primeNumbers (k,10) by XBOOLE_0:3;
reconsider x = x as Prime by A9, NEWTON:def 6;
A10: 1 + k <= x by A9, CALCUL_2:1;

per cases ( x in (multiples 2) /\ (seq (k,10)) or x in {m} ) by A8, XBOOLE_0:def 3;

suppose x in (multiples 2) /\ (seq (k,10)) ; :: thesis: contradiction

then ( x = 1 or x = 2 ) by Th62, INT_2:def 4;
hence contradiction by A7, A10, XXREAL_0:2; :: thesis: verum

end;

suppose x in {m} ; :: thesis: contradiction

then x = m by TARSKI:def 1;
hence contradiction by A7, A10, Th60; :: thesis: verum

end;

end;

end;

then A11: card ((((multiples 2) /\ (seq (k,10))) \/ {m}) \/ (primeNumbers (k,10))) = 6 + (card (primeNumbers (k,10))) by A5, CARD_2:40;
{m} c= seq (k,10) by A2, ZFMISC_1:31;
then ((multiples 2) /\ (seq (k,10))) \/ {m} c= seq (k,10) by XBOOLE_1:8;
then (((multiples 2) /\ (seq (k,10))) \/ {m}) \/ (primeNumbers (k,10)) c= seq (k,10) by XBOOLE_1:8;
then card (primeNumbers (k,10)) <= 10 - 6 by A6, A11, XREAL_1:19, NAT_1:43;
hence card (primeNumbers (k,10)) <= 4 ; :: thesis: verum

end;

end;