let 0L be lower-bounded Lattice; :: thesis: for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
let B1, B2 be Finite_Subset of the carrier of 0L; :: thesis: (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
set J = the L_join of 0L;
A1: ( the L_join of 0L is idempotent & the L_join of 0L is commutative & the L_join of 0L is associative & the L_join of 0L is having_a_unity ) by LATTICE2:26, LATTICE2:27, LATTICE2:29, LATTICE2:67;
thus FinJoin (B1 \/ B2) = the L_join of 0L $$ (B1 \/ B2),(id 0L) by LATTICE2:def 3
.= (the L_join of 0L $$ B1,(id 0L)) "\/" (the L_join of 0L $$ B2,(id 0L)) by A1, SETWISEO:42
.= (FinJoin B1) "\/" (the L_join of 0L $$ B2,(id 0L)) by LATTICE2:def 3
.= (FinJoin B1) "\/" (FinJoin B2) by LATTICE2:def 3 ; :: thesis: verum