theorem :: LATTICE3:43
for C being complete Lattice
for a, b being Element of C holds
( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )