for L being non empty LattStr
for S being non empty SubLattStr of L
for x1, x2 being Element of L
for y1, y2 being Element of S st x1 = y1 & x2 = y2 holds
x1 "/\" x2 = y1 "/\" y2