let k be Element of NAT ; :: thesis: for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds
b = {{}}
let a, b be Element of (SubstPoset (NAT,{k})); :: thesis: ( a <= b & a = {{}} implies b = {{}} )
assume A1: ( a <= b & a = {{}} ) ; :: thesis: b = {{}}
Top (SubstPoset (NAT,{k})) = {{}} by Th36;
hence b = {{}} by A1, WAYBEL15:3; :: thesis: verum