set S = the correct Lawson TopAugmentation of N;

( InclPoset the topology of the correct Lawson TopAugmentation of N is complete & not InclPoset the topology of the correct Lawson TopAugmentation of N is trivial ) ;

hence ( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial ) by WAYBEL19:def 4; :: thesis: verum

( InclPoset the topology of the correct Lawson TopAugmentation of N is complete & not InclPoset the topology of the correct Lawson TopAugmentation of N is trivial ) ;

hence ( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial ) by WAYBEL19:def 4; :: thesis: verum