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

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

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

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

thus FinJoin (B \/ {.b.}) = (FinJoin (B,(id 0L))) "\/" ((id 0L) . b) by Th13

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

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

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

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

thus FinJoin (B \/ {.b.}) = (FinJoin (B,(id 0L))) "\/" ((id 0L) . b) by Th13

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