let 1L be upper-bounded Lattice; :: thesis: for B being Element of Fin 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 Element of Fin 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:35

.= FinMeet (B,(g * f)) by LATTICE2:def 4 ; :: thesis: verum

for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))

let B be Element of Fin 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:35

.= FinMeet (B,(g * f)) by LATTICE2:def 4 ; :: thesis: verum