let M be non empty MetrStruct ; :: thesis: for S being SetSequence of M
for F being Subset-Family of (TopSpaceMetr M) st F = rng S holds
( ( S is open implies F is open ) & ( S is closed implies F is closed ) )
let S be SetSequence of M; :: thesis: for F being Subset-Family of (TopSpaceMetr M) st F = rng S holds
( ( S is open implies F is open ) & ( S is closed implies F is closed ) )
set T = TopSpaceMetr M;
let F be Subset-Family of (TopSpaceMetr M); :: thesis: ( F = rng S implies ( ( S is open implies F is open ) & ( S is closed implies F is closed ) ) )
assume A1: F = rng S ; :: thesis: ( ( S is open implies F is open ) & ( S is closed implies F is closed ) )
thus ( S is open implies F is open ) :: thesis: ( S is closed implies F is closed )
proof
assume A2: S is open ; :: thesis: F is open
let P be Subset of (TopSpaceMetr M); :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
then consider x being object such that
A3: x in dom S and
A4: S . x = P by A1, FUNCT_1:def 3;
reconsider x = x as Nat by A3;
S . x is open by A2;
hence P is open by A4, Th6; :: thesis: verum
end;
assume A5: S is closed ; :: thesis: F is closed
let P be Subset of (TopSpaceMetr M); :: according to TOPS_2:def 2 :: thesis: ( not P in F or P is closed )
assume P in F ; :: thesis: P is closed
then consider x being object such that
A6: x in dom S and
A7: S . x = P by A1, FUNCT_1:def 3;
reconsider x = x as Nat by A6;
S . x is closed by A5;
hence P is closed by A7, Th6; :: thesis: verum