for L being LATTICE
for a, b, c being Element of L st a \ b <= c & b \ a <= c holds
a \+\ b <= c by Th9;