for L being with_infima Poset
for I, J being Ideal of L holds I /\ J is Ideal of L