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

A1: now :: thesis: for a being Element of C holds
( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) )

let a be Element of C; :: thesis: ( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) )
{} is_less_than ("\/" ({},C)) "/\" a ;
then A2: "\/" ({},C) [= ("\/" ({},C)) "/\" a by Def21;
A3: ("\/" ({},C)) "/\" a [= "\/" ({},C) by LATTICES:6;
hence ("\/" ({},C)) "/\" a = "\/" ({},C) by A2, LATTICES:8; :: thesis: a "/\" ("\/" ({},C)) = "\/" ({},C)
thus a "/\" ("\/" ({},C)) = "\/" ({},C) by A2, A3, LATTICES:8; :: thesis: verum

end;

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