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