for L being transitive antisymmetric with_infima RelStr
for x, y, z being Element of L st x <= y holds
x "/\" z <= y "/\" z