let 1L be upper-bounded Lattice; for B being Element of Fin 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 Element of Fin 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 Element of 1L; 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; FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
set M = the L_meet of 1L;
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 SETWISEO:32
.=
(FinMeet (B,f)) "/\" (f . b)
by LATTICE2:def 4
; verum