let 1L be upper-bounded Lattice; :: thesis: for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L
let f be Function of the carrier of 1L, the carrier of 1L; :: thesis: FinMeet (({}. the carrier of 1L),f) = Top 1L
set M = the L_meet of 1L;
thus FinMeet (({}. the carrier of 1L),f) = the L_meet of 1L $$ (({}. the carrier of 1L),f) by LATTICE2:def 4
.= the_unity_wrt the L_meet of 1L by SETWISEO:31
.= Top 1L by LATTICE2:57 ; :: thesis: verum