take Kurat14Set ({} T) ; :: thesis: ( Kurat14Set ({} T) is compl-closed & Kurat14Set ({} T) is Cl-closed & not Kurat14Set ({} T) is empty )
thus ( Kurat14Set ({} T) is compl-closed & Kurat14Set ({} T) is Cl-closed & not Kurat14Set ({} T) is empty ) ; :: thesis: verum