theorem LatWal1: :: LATWAL_2:11
for W being WA-Lattice
for a, b, c being Element of W st a <= c & b <= c holds
a "\/" b <= c by YELLOW_0:22;