for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds (x "/\") " {x} = uparrow x