assume SubstLatt NAT ,{m} is complete ; :: thesis: contradiction
then reconsider K = SubstLatt NAT ,{m} as complete Lattice ;
( LattPOSet K is complete & not SubstPoset NAT ,{m} is complete ) ;
hence contradiction ; :: thesis: verum