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: 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 :: thesis: for x being set st x in b holds
ex y being set st
( y in a & y c= x )
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; :: thesis: verum
end;
hence a >= b by Th12; :: thesis: verum
end;
a is_<=_than {} ;
then a = "/\" ({},(SubstPoset (NAT,{k}))) by A1, YELLOW_0:31;
hence Top (SubstPoset (NAT,{k})) = {{}} by YELLOW_0:def 12; :: thesis: verum