for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L))
for X, Y being Subset of L st x = X & y = Y holds
x "\/" y = downarrow (X "\/" Y)