ex x being object st x in X by XBOOLE_0:def 1;
hence not subset-closed_closure_of X is empty by Th2; :: thesis: verum