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