let X be Subset of T; :: according to ROUGHS_2:def 18 :: thesis: (IntMap T) . X is open
(IntMap T) . X = Int X by Def16;
hence (IntMap T) . X is open ; :: thesis: verum