take {([#] X)} ; :: thesis: ( not {([#] X)} is empty & {([#] X)} is with_non-empty_elements )
thus not {([#] X)} is empty ; :: thesis: {([#] X)} is with_non-empty_elements
assume {} in {([#] X)} ; :: according to SETFAM_1:def 8 :: thesis: contradiction
hence contradiction by TARSKI:def 1; :: thesis: verum