let n be Element of NAT ; :: thesis: for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}
let a be Element of (SubstPoset (NAT,{n})); :: thesis: ( {} in a implies a = {{}} )
assume A1: {} in a ; :: thesis: a = {{}}
SubstitutionSet (NAT,{n}) = the carrier of (SubstPoset (NAT,{n})) by SUBSTLAT:def 4;
then A2: a in SubstitutionSet (NAT,{n}) ;
assume a <> {{}} ; :: thesis: contradiction
then ex k being set st
( k in a & k <> {} ) by A1, Lm9;
hence contradiction by A2, A1, SUBSTLAT:5, XBOOLE_1:2; :: thesis: verum