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 S_{1}[ 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 & S_{1}[z,z1] )

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 & S_{1}[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 } ;

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 )

X is filtered

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 } ;

A31: y in wayabove x by A1, WAYBEL_3:8;

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

take F ; :: thesis: ( y in F & F c= wayabove x )

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 S

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 & S

proof

consider f being Function of W,W such that
let z be Element of L; :: thesis: ( z in W implies ex z1 being Element of L st

( z1 in W & S_{1}[z,z1] ) )

assume z in W ; :: thesis: ex z1 being Element of L st

( z1 in W & S_{1}[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 & S_{1}[z,z1] )
by A4; :: thesis: verum

end;( z1 in W & S

assume z in W ; :: thesis: ex z1 being Element of L st

( z1 in W & S

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 & S

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 & S

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

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;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;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

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

A26:
for X being Subset of L st X in V holds
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

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;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 S_{2}[ Nat] means (iter (f,(n + (In ($1,NAT))))) . y1 <= (iter (f,n)) . y1;

A16: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[ 0 ]
;

let k be Element of NAT ; :: thesis: (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1

for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A21, A16);

then S_{2}[k]
;

hence (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; :: thesis: verum

end;defpred S

A16: for k being Nat st S

S

proof

A21:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A17: (iter (f,(n + (In (k,NAT))))) . y1 <= (iter (f,n)) . y1 ; :: thesis: S_{2}[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 S_{2}[k + 1]
by A17, A20, ORDERS_2:3; :: thesis: verum

end;assume A17: (iter (f,(n + (In (k,NAT))))) . y1 <= (iter (f,n)) . y1 ; :: thesis: S

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 S

let k be Element of NAT ; :: thesis: (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1

for k being Nat holds S

then S

hence (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; :: thesis: verum

A22: now :: thesis: uparrow (z1 "/\" z2) in Vend;

z1 "/\" z2 <= z2
by YELLOW_0:23;per cases
( n1 <= n2 or n2 <= n1 )
;

end;

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

X is filtered

proof

y <= y
;
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;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

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

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;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;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

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 )

dom f = W
by FUNCT_2:def 1;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;( 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

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

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;
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;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

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

hence
( y in F & F c= wayabove x )
by A27, A47, TARSKI:def 4; :: thesis: verumu1 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;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