let k be Element of NAT ; :: thesis: Bottom (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:1;
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
for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ;
hence a <= b by Th12; :: thesis: verum

end;

a is_>=_than {} ;
then a = "\/" ({},(SubstPoset (NAT,{k}))) by A1, YELLOW_0:30;
hence Bottom (SubstPoset (NAT,{k})) = {} by YELLOW_0:def 11; :: thesis: verum