let N be complete Lawson TopLattice; :: thesis: sigma N c= lambda N
set Z = { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } ;
{ (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } is Basis of N by WAYBEL19:32;
then { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= the topology of N by TOPS_2:64;
then A1: { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= lambda N by Th9;
sigma N c= { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } by Th8;
hence sigma N c= lambda N by A1; :: thesis: verum