let L be 0_Lattice; :: thesis: Bottom L is_a_unity_wrt the L_join of L
now :: thesis: for u being Element of L holds the L_join of L . ((Bottom L),u) = u
let u be Element of L; :: thesis: the L_join of L . ((Bottom L),u) = u
thus the L_join of L . ((Bottom L),u) = (Bottom L) "\/" u
.= u ; :: thesis: verum
end;
hence Bottom L is_a_unity_wrt the L_join of L by BINOP_1:4; :: thesis: verum