for L being Semilattice
for x, y being Element of (InclPoset (Ids L))
for x1, y1 being Subset of L st x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1