for P being Subset of T st P in Kurat14Set A holds
P ` in Kurat14Set A by Th6;
hence Kurat14Set A is compl-closed by PROB_1:def 1; :: thesis: verum