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

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