let T be non empty TopSpace; :: thesis: for A being Subset of T holds card (Kurat14Set A) <= 14
let A be Subset of T; :: thesis: card (Kurat14Set A) <= 14
set X = {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )};
set Y = {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )};
( card {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} <= 7 & card {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} <= 7 ) by CARD_2:74;
then ( card ({A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} \/ {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )}) <= (card {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )}) + (card {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )}) & (card {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )}) + (card {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )}) <= 7 + 7 ) by CARD_2:62, XREAL_1:9;
hence card (Kurat14Set A) <= 14 by XXREAL_0:2; :: thesis: verum