let T be TopSpace; :: thesis: for F being Subset-Family of
for A being Subset of st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let F be Subset-Family of ; :: thesis: for A being Subset of st A in F holds
( meet (Cl F) c= Cl A & Cl A c= union (Cl F) )
let A be Subset of ; :: 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 : ex B being Subset of 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:4; :: thesis: Cl A c= union (Cl F)
thus Cl A c= union (Cl F) by A1, ZFMISC_1:92; :: thesis: verum