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 = {{} } )
A1: Top (SubstPoset NAT ,{k}) = {{} } by Th39;
assume ( a <= b & a = {{} } ) ; :: thesis: b = {{} }
hence b = {{} } by A1, WAYBEL15:5; :: thesis: verum