for C being complete Lattice holds
( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) )