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 ; :: thesis: verum