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 Th40;
hence a = {} by A1, YELLOW_5:22; :: thesis: verum