for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1
for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T