let 1L be upper-bounded Lattice; :: thesis: for B being Finite_Subset of the carrier of 1L
for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet (B \/ {.b.}),f = (FinMeet B,f) "/\" (f . b)
let B be Finite_Subset of the carrier of 1L; :: thesis: for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet (B \/ {.b.}),f = (FinMeet B,f) "/\" (f . b)
let b be Element of 1L; :: thesis: for f being UnOp of the carrier of 1L holds FinMeet (B \/ {.b.}),f = (FinMeet B,f) "/\" (f . b)
let f be UnOp of the carrier of 1L; :: thesis: FinMeet (B \/ {.b.}),f = (FinMeet B,f) "/\" (f . b)
set M = the L_meet of 1L;
A1: ( the L_meet of 1L is idempotent & the L_meet of 1L is commutative ) by LATTICE2:30, LATTICE2:31;
A2: the L_meet of 1L is associative by LATTICE2:32;
thus FinMeet (B \/ {.b.}),f = the L_meet of 1L $$ (B \/ {.b.}),f by LATTICE2:def 4
.= (the L_meet of 1L $$ B,f) "/\" (f . b) by A1, A2, LATTICE2:73, SETWISEO:41
.= (FinMeet B,f) "/\" (f . b) by LATTICE2:def 4 ; :: thesis: verum