theorem Th15: :: WAYBEL14:15

for P being non empty complete Poset
for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }