theorem Th23: :: LATTICE4:23

for 1L being upper-bounded Lattice
for B1, B2 being Element of Fin the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)