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