set A = KurExSet ;
A1: card ((Kurat14ClPart KurExSet ) \/ (Kurat14OpPart KurExSet )) = 6 + 6 by Th60, Th62, Th63, CARD_2:53
.= 12 ;
set B = {KurExSet ,(KurExSet ` )};
A2: {KurExSet ,(KurExSet ` )} misses (Kurat14ClPart KurExSet ) \/ (Kurat14OpPart KurExSet ) by Th64, Th66, XBOOLE_1:70;
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 A2, CARD_2:53
.= 2 + 12 by A1, Th65, CARD_2:76
.= 14 ;
hence card (Kurat14Set KurExSet ) = 14 ; :: thesis: verum