for L being Lattice
for a, b being Element of L st a [= b holds
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9