for K being reflexive antisymmetric with_suprema with_infima RelStr
for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1