let L be Lattice; :: thesis: ( the L_join of L is having_a_unity implies Bottom L = the_unity_wrt the L_join of L )
set J = the L_join of L;
given u being Element of L such that A1: u is_a_unity_wrt the L_join of L ; :: according to SETWISEO:def 2 :: thesis: Bottom L = the_unity_wrt the L_join of L
the L_join of L is commutative by Th27;
then for v being Element of L holds the L_join of L . u,v = v by A1, BINOP_1:12;
then u = Bottom L by Th22;
hence Bottom L = the_unity_wrt the L_join of L by A1, BINOP_1:def 8; :: thesis: verum