let n be Nat; :: thesis: ( 0 <= n & n < 6 implies card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13 )
assume A1: ( 0 <= n & n < 6 ) ; :: thesis: card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13
set M2 = multiples 2;
set M3 = multiples 3;
set M23 = (multiples 2) \/ (multiples 3);
A2: (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) misses (seq ((n + 3),(6 * 3))) /\ ((multiples 2) \/ (multiples 3)) by Th75, XBOOLE_1:76;
seq (n,(3 + (6 * 3))) = (seq (n,3)) \/ (seq ((n + 3),(6 * 3))) by Th77;
then (seq (n,(3 + 18))) /\ ((multiples 2) \/ (multiples 3)) = ((seq (n,3)) /\ ((multiples 2) \/ (multiples 3))) \/ ((seq ((n + 3),(3 * 6))) /\ ((multiples 2) \/ (multiples 3))) by XBOOLE_1:23;
then A3: card ((seq (n,(3 + (6 * 3)))) /\ ((multiples 2) \/ (multiples 3))) = (card ((seq (n,3)) /\ ((multiples 2) \/ (multiples 3)))) + (card ((seq ((n + 3),(6 * 3))) /\ ((multiples 2) \/ (multiples 3)))) by A2, CARD_2:40;
A4: card ((seq ((n + 3),(6 * 3))) /\ ((multiples 2) \/ (multiples 3))) = 12

proof

A5: ( 2 divides 2 * 3 & 3 divides 2 * 3 ) ;
(multiples 2) \/ (multiples 3) = ((multiples 2) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= (((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= ((((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6 ;
then card ((seq ((n + 3),(6 * 3))) /\ ((multiples 2) \/ (multiples 3))) = 3 * (card ((seq ((0 * 6),6)) /\ ((multiples 2) \/ (multiples 3)))) by A5, Th90
.= 3 * 4 by Th91 ;
hence card ((seq ((n + 3),(6 * 3))) /\ ((multiples 2) \/ (multiples 3))) = 12 ; :: thesis: verum

end;

A6: for i, n being Nat holds
( i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) iff ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) ) )

proof

let i, n be Nat; :: thesis: ( i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) iff ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) ) )

hereby :: thesis: ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) implies i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) )

assume A7: i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) ; :: thesis: ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) )
( i in multiples 2 or i in multiples 3 ) by A7, XBOOLE_0:def 3;
hence ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) ) by A7, NUMBER14:62, Th73; :: thesis: verum

end;

assume ( n < i & i <= n + 3 & ( 2 divides i or 3 divides i ) ) ; :: thesis: i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3))
then A8: ( ( i in multiples 2 or i in multiples 3 ) & i in seq (n,3) ) by Th73, NUMBER14:62;
then i in (multiples 2) \/ (multiples 3) by XBOOLE_0:def 3;
hence i in (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) by A8, XBOOLE_0:def 4; :: thesis: verum

end;

not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty

proof

n < 5 + 1 by A1;
then n <= 5 by NAT_1:13;
then not not n = 0 & ... & not n = 5 ;

per cases then ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) ;

suppose ( n = 0 or n = 1 ) ; :: thesis: not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty

then ( n < 2 & 2 <= n + 3 & 2 divides 2 ) ;
hence not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty by A6; :: thesis: verum

end;

suppose ( n = 2 or n = 3 ) ; :: thesis: not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty

then ( n < 2 * 2 & 2 * 2 <= n + 3 & 2 divides 2 * 2 ) ;
hence not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty by A6; :: thesis: verum

end;

suppose ( n = 4 or n = 5 ) ; :: thesis: not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty

then ( n < 2 * 3 & 2 * 3 <= n + 3 & 2 divides 2 * 3 ) ;
hence not (seq (n,3)) /\ ((multiples 2) \/ (multiples 3)) is empty by A6; :: thesis: verum

end;

end;

end;

then card ((seq (n,(3 + (6 * 3)))) /\ ((multiples 2) \/ (multiples 3))) >= 12 + 1 by A3, A4, NAT_1:14, XREAL_1:6;
hence card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13 ; :: thesis: verum