let k be Element of NAT ; :: thesis: for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds
a = {}
let a, b be Element of (SubstPoset (NAT,{k})); :: thesis: ( a <= b & b = {} implies a = {} )
assume A1: ( a <= b & b = {} ) ; :: thesis: a = {}
Bottom (SubstPoset (NAT,{k})) = {} by Th37;
hence a = {} by A1, YELLOW_5:19; :: thesis: verum