( bool X is with_empty_element cap-closed semi-diff-closed Subset-Family of X & X c= X ) ;
hence ex b₁ being with_empty_element cap-closed semi-diff-closed Subset-Family of X st X in b₁ ; :: thesis: verum