let F be sequence of (bool NAT); :: thesis: ( ( for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ) implies rng F is basis of (Frechet_Filter NAT) )
assume A1: for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ; :: thesis: rng F is basis of (Frechet_Filter NAT)
A2: Frechet_Filter NAT = { (NAT \ A) where A is finite Subset of NAT : verum } by Th24;
for t being object st t in rng F holds
t in Frechet_Filter NAT
proof
let t be object ; :: thesis: ( t in rng F implies t in Frechet_Filter NAT )
assume A3: t in rng F ; :: thesis: t in Frechet_Filter NAT
then consider x0 being object such that
A4: ( x0 in dom F & t = F . x0 ) by FUNCT_1:def 3;
reconsider x2 = x0 as natural number by A4;
reconsider t1 = t as Subset of NAT by A3;
A5: now :: thesis: ( NAT \ t1 is finite & NAT \ t1 is Subset of NAT )
NAT \ t1 = NAT \ { y where y is Element of NAT : x2 <= y } by A1, A4;
hence NAT \ t1 is finite by Th22; :: thesis: NAT \ t1 is Subset of NAT
thus NAT \ t1 is Subset of NAT ; :: thesis: verum
end;
NAT \ (NAT \ t1) = t1 /\ NAT by XBOOLE_1:48;
then t1 = NAT \ (NAT \ t1) by XBOOLE_1:17, XBOOLE_1:19;
hence t in Frechet_Filter NAT by A2, A5; :: thesis: verum
end;
then rng F c= Frechet_Filter NAT ;
then reconsider F1 = rng F as non empty Subset of (Frechet_Filter NAT) ;
A7: F1 is filter_basis
proof
for f being Element of Frechet_Filter NAT ex b being Element of F1 st b c= f
proof
let f be Element of Frechet_Filter NAT; :: thesis: ex b being Element of F1 st b c= f
f in { (NAT \ A) where A is finite Subset of NAT : verum } by A2;
then consider A0 being finite Subset of NAT such that
A8: f = NAT \ A0 ;
reconsider A1 = A0 as natural-membered set ;
consider n0 being natural number such that
A9: A1 c= Segm n0 by AFINSQ_2:2;
reconsider n1 = n0 as Element of NAT by ORDINAL1:def 12;
A10: dom F = NAT by FUNCT_2:def 1;
set b = NAT \ (Segm n0);
NAT \ (Segm n0) is Element of rng F
proof
NAT \ (Segm n0) = { y where y is Element of NAT : n0 <= y }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { y where y is Element of NAT : n0 <= y } c= NAT \ (Segm n0)
let x be object ; :: thesis: ( x in NAT \ (Segm n0) implies x in { y where y is Element of NAT : n0 <= y } )
assume A11: x in NAT \ (Segm n0) ; :: thesis: x in { y where y is Element of NAT : n0 <= y }
then reconsider x1 = x as Element of NAT ;
for n0 being natural number
for t being Element of NAT \ (Segm n0) holds n0 <= t
proof
let n0 be natural number ; :: thesis: for t being Element of NAT \ (Segm n0) holds n0 <= t
let t be Element of NAT \ (Segm n0); :: thesis: n0 <= t
Segm n0 c< NAT ;
then not NAT \ (Segm n0) is empty by XBOOLE_1:105;
then not t in Segm n0 by XBOOLE_0:def 5;
hence n0 <= t by NAT_1:44; :: thesis: verum
end;
then n0 <= x1 by A11;
hence x in { y where y is Element of NAT : n0 <= y } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of NAT : n0 <= y } or x in NAT \ (Segm n0) )
assume x in { y where y is Element of NAT : n0 <= y } ; :: thesis: x in NAT \ (Segm n0)
then consider y0 being Element of NAT such that
A12: x = y0 and
A13: n0 <= y0 ;
reconsider x1 = x as Element of NAT by A12;
( x1 in NAT & not x1 in Segm n0 ) by A12, A13, NAT_1:44;
hence x in NAT \ (Segm n0) by XBOOLE_0:def 5; :: thesis: verum
end;
then NAT \ (Segm n0) = F . n1 by A1;
hence NAT \ (Segm n0) is Element of rng F by A10, FUNCT_1:3; :: thesis: verum
end;
hence ex b being Element of F1 st b c= f by A8, A9, XBOOLE_1:34; :: thesis: verum
end;
hence F1 is filter_basis ; :: thesis: verum
end;
thus rng F is basis of (Frechet_Filter NAT) by A7; :: thesis: verum