theorem Th14: :: LATTICE4:14

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