let 1L be upper-bounded Lattice; :: thesis: for B being Finite_Subset of the carrier of 1L
for f, g being UnOp of the carrier of 1L holds FinMeet (f .: B),g = FinMeet B,(g * f)
let B be Finite_Subset of the carrier of 1L; :: thesis: for f, g being UnOp of the carrier of 1L holds FinMeet (f .: B),g = FinMeet B,(g * f)
let f, g be UnOp of the carrier of 1L; :: thesis: FinMeet (f .: B),g = FinMeet B,(g * f)
set M = the L_meet of 1L;
thus FinMeet (f .: B),g = the L_meet of 1L $$ (f .: B),g by LATTICE2:def 4
.= the L_meet of 1L $$ B,(g * f) by SETWISEO:44
.= FinMeet B,(g * f) by LATTICE2:def 4 ; :: thesis: verum