theorem :: RLSUB_2:64

for l being Lattice
for b being Element of l st ( for a being Element of l holds a "/\" b = b ) holds
b = Bottom l by Lm19;