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

proof

assume A2: S is open ; :: thesis: S9 is open
let i be Nat; :: according to COMPL_SP:def 5 :: thesis: S9 . i is open
S . i is open by A2;
hence S9 . i is open by A1, Th6; :: thesis: verum

end;

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

proof

assume A3: S9 is open ; :: thesis: S is open
let i be Nat; :: according to COMPL_SP:def 7 :: thesis: S . i is open
S9 . i is open by A3;
hence S . i is open by A1, Th6; :: thesis: verum

end;

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

proof

assume A4: S is closed ; :: thesis: S9 is closed
let i be Nat; :: according to COMPL_SP:def 6 :: thesis: S9 . i is closed
S . i is closed by A4;
hence S9 . i is closed by A1, Th6; :: thesis: verum

end;

assume A5: S9 is closed ; :: thesis: S is closed
let i be Nat; :: according to COMPL_SP:def 8 :: thesis: S . i is closed
S9 . i is closed by A5;
hence S . i is closed by A1, Th6; :: thesis: verum