take Y = {{0 }}; :: thesis: ( Y is mutually-disjoint & not Y is empty & Y is with_non-empty_elements )
thus ( Y is mutually-disjoint & not Y is empty & Y is with_non-empty_elements ) by TAXONOM2:10; :: thesis: verum