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