theorem :: LATTICE3:49

for C being complete Lattice holds
( C is 0_Lattice & Bottom C = "\/" ({},C) )