let X be set ; :: thesis: ( X is with_zero implies not X is with_non-empty_elements )
assume X is with_zero ; :: thesis: not X is with_non-empty_elements
hence {} in X ; :: according to SETFAM_1:def 8 :: thesis: verum