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