theorem Th91: :: NUMBER19:91
for n being Nat holds
( 4 = card ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3))) & {((6 * n) + 1),((6 * n) + 5)} = (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) )