let L be lower-bounded Lattice; :: thesis: Bottom L = Bottom (LattPOSet L)
set x = % (Bottom (LattPOSet L));
now :: thesis: for a being Element of L holds
( (% (Bottom (LattPOSet L))) "/\" a = % (Bottom (LattPOSet L)) & a "/\" (% (Bottom (LattPOSet L))) = % (Bottom (LattPOSet L)) )
let a be Element of L; :: thesis: ( (% (Bottom (LattPOSet L))) "/\" a = % (Bottom (LattPOSet L)) & a "/\" (% (Bottom (LattPOSet L))) = % (Bottom (LattPOSet L)) )
a % >= (% (Bottom (LattPOSet L))) % by YELLOW_0:44;
then % (Bottom (LattPOSet L)) [= a by LATTICE3:7;
hence ( (% (Bottom (LattPOSet L))) "/\" a = % (Bottom (LattPOSet L)) & a "/\" (% (Bottom (LattPOSet L))) = % (Bottom (LattPOSet L)) ) by LATTICES:4; :: thesis: verum
end;
hence Bottom L = Bottom (LattPOSet L) by LATTICES:def 16; :: thesis: verum