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