reconsider n0 = 0 as Element of OrderedNAT ;
A1: uparrow n0 = uparrow {n0} ;
uparrow {n0} = NAT

proof

NAT c= uparrow {n0}

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in NAT or t in uparrow {n0} )
assume t in NAT ; :: thesis: t in uparrow {n0}
then reconsider t0 = t as Element of OrderedNAT ;
( n0 <= t0 & n0 in {n0} ) by TARSKI:def 1;
hence t in uparrow {n0} by WAYBEL_0:def 16; :: thesis: verum

end;

hence uparrow {n0} = NAT ; :: thesis: verum

end;

hence NAT in base_of_frechet_filter by A1; :: thesis: verum