let 1L be upper-bounded Lattice; :: thesis: for B being Element of Fin the carrier of 1L

for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

let B be Element of Fin the carrier of 1L; :: thesis: for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

let b be Element of 1L; :: thesis: FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

thus FinMeet (B \/ {.b.}) = (FinMeet (B,(id 1L))) "/\" ((id 1L) . b) by Th20

.= (FinMeet B) "/\" b by FUNCT_1:18 ; :: thesis: verum

for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

let B be Element of Fin the carrier of 1L; :: thesis: for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

let b be Element of 1L; :: thesis: FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

thus FinMeet (B \/ {.b.}) = (FinMeet (B,(id 1L))) "/\" ((id 1L) . b) by Th20

.= (FinMeet B) "/\" b by FUNCT_1:18 ; :: thesis: verum