consider b being non empty set such that
A1: b in X by SETFAM_1:def 10;
b in subset-closed_closure_of X by A1, Th2;
hence not subset-closed_closure_of X is empty-membered ; :: thesis: verum