let M be MetrStruct ; :: thesis: for A being Subset of M
for A9 being Subset of (TopSpaceMetr M) st A9 = A holds
( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )
let A be Subset of M; :: thesis: for A9 being Subset of (TopSpaceMetr M) st A9 = A holds
( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )
let A9 be Subset of (TopSpaceMetr M); :: thesis: ( A9 = A implies ( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) ) )
assume A1: A9 = A ; :: thesis: ( ( A is open implies A9 is open ) & ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )
thus ( A is open implies A9 is open ) by A1, PRE_TOPC:def 2; :: thesis: ( ( A9 is open implies A is open ) & ( A is closed implies A9 is closed ) & ( A9 is closed implies A is closed ) )
thus ( A9 is open implies A is open ) by PRE_TOPC:def 2, A1; :: thesis: ( A is closed iff A9 is closed )
thus ( A is closed implies A9 is closed ) :: thesis: ( A9 is closed implies A is closed )

proof

assume A is closed ; :: thesis: A9 is closed
then A ` is open ;
then A ` in Family_open_set M ;
then A9 ` is open by A1, PRE_TOPC:def 2;
hence A9 is closed by TOPS_1:3; :: thesis: verum

end;

assume A9 is closed ; :: thesis: A is closed
then A ` in Family_open_set M by A1, PRE_TOPC:def 2;
then A ` is open ;
hence A is closed ; :: thesis: verum