let X be Subset of T; :: according to ROUGHS_2:def 17 :: thesis: (ClMap T) . X is closed
(ClMap T) . X = Cl X by Def15;
hence (ClMap T) . X is closed ; :: thesis: verum