let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
Cl F is closed-domains-family
let F be Subset-Family of T; :: thesis: ( F is domains-family implies Cl F is closed-domains-family )
assume A1: F is domains-family ; :: thesis: Cl F is closed-domains-family
for A being Subset of T st A in Cl F holds
A is closed_condensed
proof
let A be Subset of T; :: thesis: ( A in Cl F implies A is closed_condensed )
assume A in Cl F ; :: thesis: A is closed_condensed
then consider P being Subset of T such that
A2: A = Cl P and
A3: P in F by PCOMPS_1:def 2;
reconsider P = P as Subset of T ;
P is condensed by A1, A3;
hence A is closed_condensed by A2, TDLAT_1:24; :: thesis: verum
end;
hence Cl F is closed-domains-family ; :: thesis: verum