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:40
.= Top 1L by LATTICE2:74 ; :: thesis: verum