for L being antisymmetric with_suprema RelStr
for D being Subset of L
for x being Element of L holds x is_<=_than {x} "\/" D