for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )