theorem :: RLSUB_2:65

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