theorem :: LATTICE4:16

for 0L being lower-bounded Lattice holds FinJoin ({}. the carrier of 0L) = Bottom 0L by Lm1;