for L being non empty antisymmetric complete RelStr
for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)