let L be Lattice; :: thesis: ( the L_meet of L is having_a_unity implies Top L = the_unity_wrt the L_meet of L )
set J = the L_meet of L;
given u being Element of L such that A1: u is_a_unity_wrt the L_meet of L ; :: according to SETWISEO:def 2 :: thesis: Top L = the_unity_wrt the L_meet of L
for v being Element of L holds the L_meet of L . (u,v) = v by A1, BINOP_1:4;
then u = Top L by Th17;
hence Top L = the_unity_wrt the L_meet of L by A1, BINOP_1:def 8; :: thesis: verum