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