theorem Th20: :: LATTICE4:20

for 1L being upper-bounded Lattice
for B being Element of Fin the carrier of 1L
for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)