let L be Lattice; :: thesis: for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds
u = Bottom L
let u be Element of L; :: thesis: ( ( for v being Element of L holds the L_join of L . (u,v) = v ) implies u = Bottom L )
assume for v being Element of L holds the L_join of L . (u,v) = v ; :: thesis: u = Bottom L
then for v being Element of L holds u "\/" v = v ;
hence u = Bottom L by Th14; :: thesis: verum