reconsider Z = Y as Subset of (TopSpaceMetr X) ;
Cl Z is Subset of X
;
hence
( ex b1 being Subset of X ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b1 = Cl Z ) & ( for b1, b2 being Subset of X st ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b1 = Cl Z ) & ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b2 = Cl Z ) holds
b1 = b2 ) )
; verum