let L be 1_Lattice; :: thesis: Top L is_a_unity_wrt the L_meet of L

now

let u be Element of L; :: thesis: the L_meet of L . ((Top L),u) = u
thus the L_meet of L . ((Top L),u) = (Top L) "/\" u
.= u by LATTICES:17 ; :: thesis: verum

end;

hence Top L is_a_unity_wrt the L_meet of L by BINOP_1:4; :: thesis: verum