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

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