theorem :: WAYBEL19:32

for T being complete Lawson TopLattice holds { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T