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
for v being Element of L holds the L_join of L . (u,v) = v by A1, BINOP_1:4;
then u = Bottom L by Th15;
hence Bottom L = the_unity_wrt the L_join of L by A1, BINOP_1:def 8; :: thesis: verum