for L being transitive antisymmetric with_infima RelStr st L is distributive holds
for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds
a <= b "\/" c