SubstitutionSet NAT ,{k} = the carrier of (SubstPoset NAT ,{k}) by SUBSTLAT:def 4;
then reconsider E = {{} } as Element of (SubstPoset NAT ,{k}) by SUBSTLAT:2;
take E ; :: thesis: not E is empty
thus not E is empty ; :: thesis: verum