let 1L be upper-bounded Lattice; :: thesis: 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; :: 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;
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 ; :: thesis: verum