let T be non empty TopSpace; :: thesis: for F being Subset-Family of
for A being Subset of st A in F holds
Cl A c= Cl (union F)
let F be Subset-Family of ; :: thesis: for A being Subset of st A in F holds
Cl A c= Cl (union F)
let A be Subset of ; :: thesis: ( A in F implies Cl A c= Cl (union F) )
assume A in F ; :: thesis: Cl A c= Cl (union F)
then for f being set st f in A holds
f in union F by TARSKI:def 4;
then A c= union F by TARSKI:def 3;
hence Cl A c= Cl (union F) by PRE_TOPC:49; :: thesis: verum