let 1L be upper-bounded Lattice; :: thesis: for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
let B1, B2 be Finite_Subset of the carrier of 1L; :: thesis: (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
set M = the L_meet of 1L;
A1: ( the L_meet of 1L is idempotent & the L_meet of 1L is commutative & the L_meet of 1L is associative & the L_meet of 1L is having_a_unity ) by LATTICE2:30, LATTICE2:31, LATTICE2:32, LATTICE2:73;
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 A1, SETWISEO:42
.= (FinMeet B1) "/\" (the L_meet of 1L $$ B2,(id 1L)) by LATTICE2:def 4
.= (FinMeet B1) "/\" (FinMeet B2) by LATTICE2:def 4 ; :: thesis: verum