let C be complete Lattice; :: thesis: ( C is 0_Lattice & Bottom C = "\/" ({},C) )

A1: now

let a be Element of C; :: thesis: ( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) )
{} is_less_than ("\/" ({},C)) "/\" a

proof

let b be Element of C; :: according to LATTICE3:def 17 :: thesis: ( b in {} implies b [= ("\/" ({},C)) "/\" a )
thus ( b in {} implies b [= ("\/" ({},C)) "/\" a ) ; :: thesis: verum

end;

then A2: "\/" ({},C) [= ("\/" ({},C)) "/\" a by Def21;
A3: ("\/" ({},C)) "/\" a [= "\/" ({},C) by LATTICES:23;
hence ("\/" ({},C)) "/\" a = "\/" ({},C) by A2, LATTICES:26; :: thesis: a "/\" ("\/" ({},C)) = "\/" ({},C)
thus a "/\" ("\/" ({},C)) = "\/" ({},C) by A2, A3, LATTICES:26; :: thesis: verum

end;

then C is lower-bounded by LATTICES:def 13;
hence ( C is 0_Lattice & Bottom C = "\/" ({},C) ) by A1, LATTICES:def 16; :: thesis: verum