let T be TopSpace; :: thesis: for F being Subset-Family of T
for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let F be Subset-Family of T; :: thesis: for A being Subset of T st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let A be Subset of T; :: thesis: ( A in F implies ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) )
assume A in F ; :: thesis: ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
then Cl A in { P where P is Subset of T : ex B being Subset of T st
( P = Cl B & B in F ) } ;
then A1: Cl A in Cl F by Th7;
hence meet (Cl F) c= Cl A by SETFAM_1:3; :: thesis: Cl A c= union (Cl F)
thus Cl A c= union (Cl F) by A1, ZFMISC_1:74; :: thesis: verum