for L being antisymmetric with_suprema RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_finer_than A "\/" B