let L be lower-bounded continuous LATTICE; :: thesis: for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )
let x, y be Element of L; :: thesis: ( x << y implies ex F being Open Filter of L st
( y in F & F c= wayabove x ) )
defpred S1[ Element of L, Element of L] means $2 << $1;
assume A1: x << y ; :: thesis: ex F being Open Filter of L st
( y in F & F c= wayabove x )
then reconsider W = wayabove x as non empty Subset of L by WAYBEL_3:8;
A2: for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & S1[z,z1] )
proof
let z be Element of L; :: thesis: ( z in W implies ex z1 being Element of L st
( z1 in W & S1[z,z1] ) )
assume z in W ; :: thesis: ex z1 being Element of L st
( z1 in W & S1[z,z1] )
then x << z by WAYBEL_3:8;
then consider x9 being Element of L such that
A3: x << x9 and
A4: x9 << z by WAYBEL_4:52;
x9 in W by A3, WAYBEL_3:8;
hence ex z1 being Element of L st
( z1 in W & S1[z,z1] ) by A4; :: thesis: verum
end;
consider f being Function of W,W such that
A5: for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & z1 = f . z & S1[z,z1] ) from WAYBEL_6:sch 1(A2);
 set V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ;
now :: thesis: for u1 being object st u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } holds
u1 in bool the carrier of L
let u1 be object ; :: thesis: ( u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in bool the carrier of L )
assume u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; :: thesis: u1 in bool the carrier of L
then ex z being Element of L st
( u1 = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ;
hence u1 in bool the carrier of L ; :: thesis: verum
end;
then reconsider V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset-Family of L by TARSKI:def 3;
A6: for X, Y being Subset of L st X in V & Y in V holds
ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
proof
reconsider y1 = y as Element of W by A1, WAYBEL_3:8;
let X, Y be Subset of L; :: thesis: ( X in V & Y in V implies ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) )
assume that
A7: X in V and
A8: Y in V ; :: thesis: ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
consider z2 being Element of L such that
A9: Y = uparrow z2 and
A10: ex n being Element of NAT st z2 = (iter (f,n)) . y by A8;
consider n2 being Element of NAT such that
A11: z2 = (iter (f,n2)) . y by A10;
consider z1 being Element of L such that
A12: X = uparrow z1 and
A13: ex n being Element of NAT st z1 = (iter (f,n)) . y by A7;
set z = z1 "/\" z2;
consider n1 being Element of NAT such that
A14: z1 = (iter (f,n1)) . y by A13;
A15: for n, k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
proof
let n be Element of NAT ; :: thesis: for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
defpred S2[ Nat] means (iter (f,(n + (In ($1,NAT))))) . y1 <= (iter (f,n)) . y1;
A16: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A17: (iter (f,(n + (In (k,NAT))))) . y1 <= (iter (f,n)) . y1 ; :: thesis: S2[k + 1]
set nk = (iter (f,(n + (In (k,NAT))))) . y1;
(iter (f,(n + (In (k,NAT))))) . y1 in W by FUNCT_2:5;
then consider znk being Element of L such that
znk in W and
A18: znk = f . ((iter (f,(n + (In (k,NAT))))) . y1) and
A19: znk << (iter (f,(n + (In (k,NAT))))) . y1 by A5;
dom (iter (f,(n + (In (k,NAT))))) = W by FUNCT_2:def 1;
then A20: znk = (f * (iter (f,(n + k)))) . y1 by A18, FUNCT_1:13
.= (iter (f,((n + k) + 1))) . y1 by FUNCT_7:71
.= (iter (f,(n + (k + 1)))) . y1 ;
znk <= (iter (f,(n + (In (k,NAT))))) . y1 by A19, WAYBEL_3:1;
hence S2[k + 1] by A17, A20, ORDERS_2:3; :: thesis: verum
end;
A21: S2[ 0 ] ;
let k be Element of NAT ; :: thesis: (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
for k being Nat holds S2[k] from NAT_1:sch 2(A21, A16);
 then S2[k] ;
hence (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; :: thesis: verum
end;
A22: now :: thesis: uparrow (z1 "/\" z2) in V
per cases ( n1 <= n2 or n2 <= n1 ) ;
suppose n1 <= n2 ; :: thesis: uparrow (z1 "/\" z2) in V
then consider k being Nat such that
A23: n1 + k = n2 by NAT_1:10;
k in NAT by ORDINAL1:def 12;
then z2 <= z1 by A14, A11, A15, A23;
hence uparrow (z1 "/\" z2) in V by A8, A9, YELLOW_0:25; :: thesis: verum
end;
suppose n2 <= n1 ; :: thesis: uparrow (z1 "/\" z2) in V
then consider k being Nat such that
A24: n2 + k = n1 by NAT_1:10;
k in NAT by ORDINAL1:def 12;
then z1 <= z2 by A14, A11, A15, A24;
hence uparrow (z1 "/\" z2) in V by A7, A12, YELLOW_0:25; :: thesis: verum
end;
end;
end;
z1 "/\" z2 <= z2 by YELLOW_0:23;
then A25: uparrow z2 c= uparrow (z1 "/\" z2) by WAYBEL_0:22;
z1 "/\" z2 <= z1 by YELLOW_0:23;
then uparrow z1 c= uparrow (z1 "/\" z2) by WAYBEL_0:22;
hence ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) by A12, A9, A22, A25, XBOOLE_1:8; :: thesis: verum
end;
A26: for X being Subset of L st X in V holds
X is filtered
proof
let X be Subset of L; :: thesis: ( X in V implies X is filtered )
assume X in V ; :: thesis: X is filtered
then ex z being Element of L st
( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ;
hence X is filtered ; :: thesis: verum
end;
y <= y ;
then A27: y in uparrow y by WAYBEL_0:18;
set F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ;
now :: thesis: for u1 being object st u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } holds
u1 in the carrier of L
let u1 be object ; :: thesis: ( u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in the carrier of L )
assume u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; :: thesis: u1 in the carrier of L
then consider Y being set such that
A28: u1 in Y and
A29: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def 4;
consider z being Element of L such that
A30: Y = uparrow z and
ex n being Element of NAT st z = (iter (f,n)) . y by A29;
reconsider z1 = {z} as Subset of L ;
u1 in { a where a is Element of L : ex b being Element of L st
( a >= b & b in z1 ) } by A28, A30, WAYBEL_0:15;
then ex a being Element of L st
( a = u1 & ex b being Element of L st
( a >= b & b in z1 ) ) ;
hence u1 in the carrier of L ; :: thesis: verum
end;
then reconsider F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset of L by TARSKI:def 3;
A31: y in wayabove x by A1, WAYBEL_3:8;
A32: now :: thesis: for u1 being Element of L st u1 in F holds
ex g being Element of L st
( g in F & g << u1 )
let u1 be Element of L; :: thesis: ( u1 in F implies ex g being Element of L st
( g in F & g << u1 ) )
assume u1 in F ; :: thesis: ex g being Element of L st
( g in F & g << u1 )
then consider Y being set such that
A33: u1 in Y and
A34: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def 4;
consider z being Element of L such that
A35: Y = uparrow z and
A36: ex n being Element of NAT st z = (iter (f,n)) . y by A34;
consider n being Element of NAT such that
A37: z = (iter (f,n)) . y by A36;
z in W by A31, A37, FUNCT_2:5;
then consider z9 being Element of L such that
z9 in W and
A38: z9 = f . z and
A39: z9 << z by A5;
z9 <= z9 ;
then A40: z9 in uparrow z9 by WAYBEL_0:18;
dom (iter (f,n)) = W by FUNCT_2:def 1;
then z9 = (f * (iter (f,n))) . y by A31, A37, A38, FUNCT_1:13
.= (iter (f,(n + 1))) . y by FUNCT_7:71 ;
then uparrow z9 in { (uparrow p) where p is Element of L : ex n being Element of NAT st p = (iter (f,n)) . y } ;
then A41: z9 in F by A40, TARSKI:def 4;
reconsider z1 = {z} as Subset of L ;
u1 in { a where a is Element of L : ex b being Element of L st
( a >= b & b in z1 ) } by A33, A35, WAYBEL_0:15;
then consider a being Element of L such that
A42: a = u1 and
A43: ex b being Element of L st
( a >= b & b in z1 ) ;
consider b being Element of L such that
A44: a >= b and
A45: b in z1 by A43;
b = z by A45, TARSKI:def 1;
hence ex g being Element of L st
( g in F & g << u1 ) by A42, A44, A39, A41, WAYBEL_3:2; :: thesis: verum
end;
dom f = W by FUNCT_2:def 1;
then A46: y in field f by A31, XBOOLE_0:def 3;
(iter (f,0)) . y = (id (field f)) . y by FUNCT_7:68
.= y by A46, FUNCT_1:18 ;
then A47: uparrow y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ;
for X being Subset of L st X in V holds
X is upper
proof
let X be Subset of L; :: thesis: ( X in V implies X is upper )
assume X in V ; :: thesis: X is upper
then ex z being Element of L st
( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ;
hence X is upper ; :: thesis: verum
end;
then reconsider F = F as Open Filter of L by A27, A47, A26, A6, A32, Def1, TARSKI:def 4, WAYBEL_0:28, WAYBEL_0:47;
take F ; :: thesis: ( y in F & F c= wayabove x )
now :: thesis: for u1 being object st u1 in F holds
u1 in wayabove x
let u1 be object ; :: thesis: ( u1 in F implies u1 in wayabove x )
assume A48: u1 in F ; :: thesis: u1 in wayabove x
then consider Y being set such that
A49: u1 in Y and
A50: Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } by TARSKI:def 4;
reconsider u = u1 as Element of L by A48;
consider z being Element of L such that
A51: Y = uparrow z and
A52: ex n being Element of NAT st z = (iter (f,n)) . y by A50;
z in wayabove x by A31, A52, FUNCT_2:5;
then A53: x << z by WAYBEL_3:8;
z <= u by A49, A51, WAYBEL_0:18;
then x << u by A53, WAYBEL_3:2;
hence u1 in wayabove x by WAYBEL_3:8; :: thesis: verum
end;
hence ( y in F & F c= wayabove x ) by A27, A47, TARSKI:def 4; :: thesis: verum