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