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

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