theorem Th3: :: TOPS_5:3

for A being set
for F being Subset-Family of A
for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }