reconsider S = bool X as Subset-Family of X ;
take S ; :: thesis: ( not S is empty & S is semi-diff-closed & S is cap-closed )
thus ( not S is empty & S is semi-diff-closed & S is cap-closed ) ; :: thesis: verum