for L being antisymmetric with_suprema RelStr
for A, B being Subset of L holds A "\/" B is_coarser_than A