let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; :: thesis: Bottom L = Bot' L

set Y = Bot' L;

( L is lower-bounded & ( for a being Element of L holds

( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) ) ) by Th5, Th14;

hence Bottom L = Bot' L by LATTICES:def 16; :: thesis: verum

set Y = Bot' L;

( L is lower-bounded & ( for a being Element of L holds

( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) ) ) by Th5, Th14;

hence Bottom L = Bot' L by LATTICES:def 16; :: thesis: verum