let A be with_non-empty_elements set ; :: thesis: for B being set st B c= A holds
B is with_non-empty_elements
let B be set ; :: thesis: ( B c= A implies B is with_non-empty_elements )
assume A1: B c= A ; :: thesis: B is with_non-empty_elements
assume {} in B ; :: according to SETFAM_1:def 8 :: thesis: contradiction
hence contradiction by A1; :: thesis: verum