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 = {{} } )
SubstitutionSet NAT ,{n} = the carrier of (SubstPoset NAT ,{n}) by SUBSTLAT:def 4;
then A1: a in SubstitutionSet NAT ,{n} ;
assume A2: {} in a ; :: thesis: a = {{} }
assume a <> {{} } ; :: thesis: contradiction
then consider k being set such that
A3: ( k in a & k <> {} ) by A2, Lm9;
thus contradiction by A1, A2, A3, SUBSTLAT:5, XBOOLE_1:2; :: thesis: verum