let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds card (Kurat7Set A) <= 3
let A be Subset of T; :: thesis: card (Kurat7Set A) <= 3
Kurat7Set A = {A,(Cl A),(Int A)} by Seven1;
hence card (Kurat7Set A) <= 3 by CARD_2:51; :: thesis: verum