theorem Th21: :: LATTICE4:21

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