let 0L be lower-bounded Lattice; :: thesis: for B being Finite_Subset of
for b being Element of holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
let B be Finite_Subset of ; :: thesis: for b being Element of holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
let b be Element of ; :: thesis: FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
thus FinJoin (B \/ {.b.}) = (FinJoin B,(id 0L)) "\/" ((id 0L) . b) by Th20
.= (FinJoin B) "\/" b by TMAP_1:91 ; :: thesis: verum