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

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