take Kurat14Set KurExSet ; :: thesis: ( Kurat14Set KurExSet is with_proper_subsets & Kurat14Set KurExSet is with_non-empty_elements )
thus ( Kurat14Set KurExSet is with_proper_subsets & Kurat14Set KurExSet is with_non-empty_elements ) ; :: thesis: verum