theorem Th84: :: TDLAT_2:85

for T being non empty TopSpace
for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )