theorem Th4: :: TOPS_5:4

for A being set
for F being Subset-Family of A
for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }