let n be Nat; :: thesis: ( 4 = card ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3))) & {((6 * n) + 1),((6 * n) + 5)} = (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) )
set S = seq ((6 * n),6);
set M2 = multiples 2;
set M3 = multiples 3;
( 6 * n < (6 * n) + 1 & (6 * n) + 1 <= ((6 * n) + 1) + 5 & ((6 * n) + 1) + 5 = (6 * n) + 6 ) by NAT_1:11, NAT_1:13;
then A1: (6 * n) + 1 in seq ((6 * n),6) by Th73;
( (6 * n) + 0 < (6 * n) + 5 & (6 * n) + 5 < ((6 * n) + 5) + 1 & ((6 * n) + 5) + 1 = (6 * n) + 6 ) by NAT_1:13, XREAL_1:6;
then A2: (6 * n) + 5 in seq ((6 * n),6) by Th73;
( (6 * n) + 1 = (2 * (3 * n)) + 1 & (6 * n) + 1 = (3 * (2 * n)) + 1 ) ;
then ( not (6 * n) + 1 in multiples 2 & not (6 * n) + 1 in multiples 3 ) by NUMBER14:62, NAT_4:9;
then not (6 * n) + 1 in (multiples 2) \/ (multiples 3) by XBOOLE_0:def 3;
then A3: (6 * n) + 1 in (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) by A1, XBOOLE_0:def 5;
( (6 * n) + 5 = (2 * ((3 * n) + 2)) + 1 & (6 * n) + 5 = (3 * ((2 * n) + 1)) + 2 ) ;
then ( not (6 * n) + 5 in multiples 2 & not (6 * n) + 5 in multiples 3 ) by NUMBER14:62, NAT_4:9;
then not (6 * n) + 5 in (multiples 2) \/ (multiples 3) by XBOOLE_0:def 3;
then (6 * n) + 5 in (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) by A2, XBOOLE_0:def 5;
then A4: {((6 * n) + 1),((6 * n) + 5)} c= (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) by A3, ZFMISC_1:32;
A5: (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) c= {((6 * n) + 1),((6 * n) + 5)}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) or y in {((6 * n) + 1),((6 * n) + 5)} )
assume A6: y in (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}
then reconsider y = y as Nat ;
not y in (multiples 2) \/ (multiples 3) by A6, XBOOLE_0:def 5;
then A7: ( not y in multiples 2 & not y in multiples 3 ) by XBOOLE_0:def 3;
( (6 * n) + 1 <= y & y <= (6 * n) + 6 ) by A6, CALCUL_2:1;
then not not y = ((6 * n) + 1) + 0 & ... & not y = ((6 * n) + 1) + 5 by NAT_1:62;

per cases then ( y = ((6 * n) + 1) + 0 or y = ((6 * n) + 1) + 4 or y = ((6 * n) + 1) + 1 or y = ((6 * n) + 1) + 2 or y = ((6 * n) + 1) + 3 or y = ((6 * n) + 1) + 5 ) ;

suppose ( y = ((6 * n) + 1) + 0 or y = ((6 * n) + 1) + 4 ) ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}

hence y in {((6 * n) + 1),((6 * n) + 5)} by TARSKI:def 2; :: thesis: verum

end;

suppose y = ((6 * n) + 1) + 1 ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}

then y = 2 * ((3 * n) + 1) ;
then 2 divides y ;
hence y in {((6 * n) + 1),((6 * n) + 5)} by A7, NUMBER14:62; :: thesis: verum

end;

suppose y = ((6 * n) + 1) + 2 ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}

then y = 3 * ((2 * n) + 1) ;
then 3 divides y ;
hence y in {((6 * n) + 1),((6 * n) + 5)} by A7, NUMBER14:62; :: thesis: verum

end;

suppose y = ((6 * n) + 1) + 3 ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}

then y = 2 * ((3 * n) + 2) ;
then 2 divides y ;
hence y in {((6 * n) + 1),((6 * n) + 5)} by A7, NUMBER14:62; :: thesis: verum

end;

suppose y = ((6 * n) + 1) + 5 ; :: thesis: y in {((6 * n) + 1),((6 * n) + 5)}

then y = 2 * ((3 * n) + 3) ;
then 2 divides y ;
hence y in {((6 * n) + 1),((6 * n) + 5)} by A7, NUMBER14:62; :: thesis: verum

end;

end;

end;

then A8: (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) = {((6 * n) + 1),((6 * n) + 5)} by A4, XBOOLE_0:def 10;
(6 * n) + 1 <> (6 * n) + 5 ;
then A9: card ((seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3))) = 2 by A8, CARD_2:57;
A10: card (seq ((6 * n),6)) = 6 by NUMBER14:73;
seq ((6 * n),6) = ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3))) \/ ((seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3))) ;
then 6 = (card ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3)))) + (card ((seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)))) by A10, XBOOLE_1:89, CARD_2:40;
hence ( 4 = card ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3))) & {((6 * n) + 1),((6 * n) + 5)} = (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) ) by A4, XBOOLE_0:def 10, A5, A9; :: thesis: verum