let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is open-domains-family holds
F is open
let F be Subset-Family of T; :: thesis: ( F is open-domains-family implies F is open )
assume A1: F is open-domains-family ; :: thesis: F is open
for A being Subset of T st A in F holds
A is open
proof
let A be Subset of T; :: thesis: ( A in F implies A is open )
assume A in F ; :: thesis: A is open
then A is open_condensed by A1;
hence A is open by TOPS_1:67; :: thesis: verum
end;
hence F is open by TOPS_2:def 1; :: thesis: verum