for L being with_infima Poset
for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y