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

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