take cobool X ; :: thesis: ( cobool X is diff-c=-finite-partition-closed & cobool X is diff-finite-partition-closed & cobool X is cap-finite-partition-closed & cobool X is with_empty_element )
thus ( cobool X is diff-c=-finite-partition-closed & cobool X is diff-finite-partition-closed & cobool X is cap-finite-partition-closed & cobool X is with_empty_element ) ; :: thesis: verum