let B be Element of base_of_frechet_filter ; :: thesis: ex n being Nat st B = NAT \ (Segm n)
B in # (Tails OrderedNAT) ;
then consider no being Element of OrderedNAT such that
A1: B = uparrow no ;
reconsider n = no as Nat ;
take n ; :: thesis: B = NAT \ (Segm n)
thus B = NAT \ (Segm n) by A1, Th13; :: thesis: verum