consider Z being Subset of (TopSpaceMetr X) such that
A1: ( Z = H & Cl H = Cl Z ) by Def1;
Z c= Cl Z by PRE_TOPC:18;
hence not Cl H is empty by A1; :: thesis: verum