for L being with_infima Poset
for a, b being Element of L holds inf {a,b} = a "/\" b