for 1L being upper-bounded Lattice
for F being ClosedSubset of 1L st Top 1L in F holds
for B being Element of Fin the carrier of 1L st B c= F holds
FinMeet B in F