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 & cobool X is with_countable_Cover )
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 & cobool X is with_countable_Cover ) ; :: thesis: verum