let n be Nat; :: thesis: for B being Subset of NAT st B = NAT \ (Segm n) holds
B is Element of base_of_frechet_filter
let B be Subset of NAT; :: thesis: ( B = NAT \ (Segm n) implies B is Element of base_of_frechet_filter )
assume A1: B = NAT \ (Segm n) ; :: thesis: B is Element of base_of_frechet_filter
reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;
B = uparrow no by A1, Th13;
then B in # (Tails OrderedNAT) ;
hence B is Element of base_of_frechet_filter ; :: thesis: verum