theorem Th13: :: LATTICE4:13

for 0L being lower-bounded Lattice
for B being Element of Fin the carrier of 0L
for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)