for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b