let M be MetrStruct ; :: thesis: for A being Subset of M
for A' being Subset of (TopSpaceMetr M) st A' = A holds
( ( A is open implies A' is open ) & ( A' is open implies A is open ) & ( A is closed implies A' is closed ) & ( A' is closed implies A is closed ) )
let A be Subset of M; :: thesis: for A' being Subset of (TopSpaceMetr M) st A' = A holds
( ( A is open implies A' is open ) & ( A' is open implies A is open ) & ( A is closed implies A' is closed ) & ( A' is closed implies A is closed ) )
let A' be Subset of (TopSpaceMetr M); :: thesis: ( A' = A implies ( ( A is open implies A' is open ) & ( A' is open implies A is open ) & ( A is closed implies A' is closed ) & ( A' is closed implies A is closed ) ) )
assume A1: A' = A ; :: thesis: ( ( A is open implies A' is open ) & ( A' is open implies A is open ) & ( A is closed implies A' is closed ) & ( A' is closed implies A is closed ) )
thus ( A is open implies A' is open ) :: thesis: ( ( A' is open implies A is open ) & ( A is closed implies A' is closed ) & ( A' is closed implies A is closed ) )

proof

assume A is open ; :: thesis: A' is open
then A in Family_open_set M by Def3;
hence A' is open by A1, PRE_TOPC:def 5; :: thesis: verum

end;

thus ( A' is open implies A is open ) :: thesis: ( A is closed iff A' is closed )

proof

assume A' is open ; :: thesis: A is open
then A' in Family_open_set M by PRE_TOPC:def 5;
hence A is open by A1, Def3; :: thesis: verum

end;

thus ( A is closed implies A' is closed ) :: thesis: ( A' is closed implies A is closed )

proof

assume A is closed ; :: thesis: A' is closed
then A ` is open by Def4;
then A ` in Family_open_set M by Def3;
then A' ` is open by A1, PRE_TOPC:def 5;
hence A' is closed by TOPS_1:29; :: thesis: verum

end;

assume A' is closed ; :: thesis: A is closed
then A ` in Family_open_set M by A1, PRE_TOPC:def 5;
then A ` is open by Def3;
hence A is closed by Def4; :: thesis: verum