for L being antisymmetric with_infima RelStr
for X being Subset of L
for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)