theorem :: TDLAT_2:30

for T being TopSpace
for F being Subset-Family of T st F is finite holds
Int (meet F) = meet (Int F)