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