let L be non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr ; :: thesis: Bottom L = Bot' L
A1: L is lower-bounded' by Th16;
set Y = Bottom L;
for a being Element of L holds
( (Bottom L) "\/" a = a & a "\/" (Bottom L) = a ) by LATTICES:39;
hence Bottom L = Bot' L by A1, Def4; :: thesis: verum