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

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