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