let 1L be upper-bounded Lattice; :: thesis: for B1, B2 being Element of Fin the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
let B1, B2 be Element of Fin the carrier of 1L; :: thesis: (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
set M = the L_meet of 1L;
thus FinMeet (B1 \/ B2) = the L_meet of 1L $$ ((B1 \/ B2),(id 1L)) by LATTICE2:def 4
.= ( the L_meet of 1L $$ (B1,(id 1L))) "/\" ( the L_meet of 1L $$ (B2,(id 1L))) by SETWISEO:33
.= (FinMeet B1) "/\" ( the L_meet of 1L $$ (B2,(id 1L))) by LATTICE2:def 4
.= (FinMeet B1) "/\" (FinMeet B2) by LATTICE2:def 4 ; :: thesis: verum