theorem :: LATTICE4:19

for 1L being upper-bounded Lattice holds FinMeet ({}. the carrier of 1L) = Top 1L by Lm2;