let k be Element of NAT ; :: thesis: Top (SubstPoset NAT ,{k}) = {{} }
SubstitutionSet NAT ,{k} = the carrier of (SubstPoset NAT ,{k}) by SUBSTLAT:def 4;
then reconsider a = {{} } as Element of (SubstPoset NAT ,{k}) by SUBSTLAT:2;
A1: a is_<=_than {} by YELLOW_0:6;
for b being Element of (SubstPoset NAT ,{k}) st b is_<=_than {} holds
a >= b

proof

let b be Element of (SubstPoset NAT ,{k}); :: thesis: ( b is_<=_than {} implies a >= b )
assume b is_<=_than {} ; :: thesis: a >= b

now

let x be set ; :: thesis: ( x in b implies ex y being set st
( y in a & y c= x ) )
assume x in b ; :: thesis: ex y being set st
( y in a & y c= x )
take y = {} ; :: thesis: ( y in a & y c= x )
thus ( y in a & y c= x ) by TARSKI:def 1, XBOOLE_1:2; :: thesis: verum

end;

hence a >= b by Th15; :: thesis: verum

end;

then a = "/\" {} ,(SubstPoset NAT ,{k}) by A1, YELLOW_0:31;
hence Top (SubstPoset NAT ,{k}) = {{} } by YELLOW_0:def 12; :: thesis: verum