consider S being non empty cap-closed compl-closed Subset-Family of X;
take S ; :: thesis: ( not S is empty & S is compl-closed & S is cap-closed )
thus ( not S is empty & S is compl-closed & S is cap-closed ) ; :: thesis: verum