theorem :: WAYBEL14:13

for P being with_infima Poset
for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)