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

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