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;
A1: ( the L_meet of 1L is idempotent & the L_meet of 1L is commutative & the L_meet of 1L is associative ) by LATTICE2:30, LATTICE2:31, LATTICE2:32;
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 A1, LATTICE2:73, SETWISEO:44
.= FinMeet B,(g * f) by LATTICE2:def 4 ; :: thesis: verum