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