theorem Th22: :: LATTICE4:22

for 1L being upper-bounded Lattice
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))