theorem Th30: :: WAYBEL19:30

for T being complete Lawson TopLattice holds (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T