for L being non empty RelStr
for X being Subset of L
for Y being Subset of (L opp) st X = Y holds
( fininfs X = finsups Y & finsups X = fininfs Y )