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