let L be 1_Lattice; :: thesis: the L_meet of L is having_a_unity
Top L is_a_unity_wrt the L_meet of L by Th72;
hence the L_meet of L is having_a_unity by SETWISEO:def 2; :: thesis: verum