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

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

A1: now :: thesis: for a being Element of C holds

( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) )

then
C is lower-bounded
;( ("\/" ({},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;{} 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

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