theorem Th15: :: LATTICE2:15

for L being Lattice
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