set A = KurExSet ;
set B = {KurExSet,(KurExSet `)};
A1:
{KurExSet,(KurExSet `)} misses (Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet)
by Th61, Th63, XBOOLE_1:70;
A2: card ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet)) =
6 + 6
by Th57, Th59, Th60, CARD_2:40
.=
12
;
card (Kurat14Set KurExSet) =
card (({KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet))
by Lm2
.=
card ({KurExSet,(KurExSet `)} \/ ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet)))
by XBOOLE_1:4
.=
(card {KurExSet,(KurExSet `)}) + (card ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet)))
by A1, CARD_2:40
.=
2 + 12
by A2, Th62, CARD_2:57
.=
14
;
hence
card (Kurat14Set KurExSet) = 14
; verum