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

proof

assume A2: S is open ; :: thesis: S' is open
let i be natural number ; :: according to COMPL_SP:def 5 :: thesis: S' . i is open
S . i is open by A2, Def7;
hence S' . i is open by A1, Th6; :: thesis: verum

end;

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

proof

assume A3: S' is open ; :: thesis: S is open
let i be natural number ; :: according to COMPL_SP:def 7 :: thesis: S . i is open
S' . i is open by A3, Def5;
hence S . i is open by A1, Th6; :: thesis: verum

end;

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

proof

assume A4: S is closed ; :: thesis: S' is closed
let i be natural number ; :: according to COMPL_SP:def 6 :: thesis: S' . i is closed
S . i is closed by A4, Def8;
hence S' . i is closed by A1, Th6; :: thesis: verum

end;

assume A5: S' is closed ; :: thesis: S is closed
let i be natural number ; :: according to COMPL_SP:def 8 :: thesis: S . i is closed
S' . i is closed by A5, Def6;
hence S . i is closed by A1, Th6; :: thesis: verum