let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds card (Kurat14Set A) <= 6
let A be Subset of T; :: thesis: card (Kurat14Set A) <= 6
Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)} by Fourteen;
hence card (Kurat14Set A) <= 6 by CARD_2:54; :: thesis: verum