let L be lower-bounded continuous LATTICE; :: thesis: for V being upper Open Subset of L

for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let V be upper Open Subset of L; :: thesis: for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let F be Filter of L; :: thesis: for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let v be Element of L; :: thesis: ( V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable implies ex O being Open Filter of L st

( O c= V & v in O & F c= O ) )

assume that

A1: V "/\" F c= V and

A2: v in V ; :: thesis: ( for A being non empty GeneratorSet of F holds not A is countable or ex O being Open Filter of L st

( O c= V & v in O & F c= O ) )

reconsider V1 = V as non empty upper Open Subset of L by A2;

reconsider v1 = v as Element of V1 by A2;

reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th23, Th24, Th25;

given A being non empty GeneratorSet of F such that A3: A is countable ; :: thesis: ex O being Open Filter of L st

( O c= V & v in O & F c= O )

consider f being sequence of A such that

A4: rng f = A by A3, CARD_3:96;

reconsider f = f as sequence of the carrier of L by FUNCT_2:7;

deffunc H_{1}( Element of NAT ) -> Element of the carrier of L = "/\" ( { (f . m) where m is Element of NAT : m <= $1 } ,L);

consider g being sequence of the carrier of L such that

A5: for n being Element of NAT holds g . n = H_{1}(n)
from FUNCT_2:sch 4();

defpred S_{1}[ Nat, set , set ] means ex x1, y1 being Element of V1 ex z1 being Element of L st

( x1 = $2 & y1 = $3 & z1 = g . ($1 + 1) & y1 << x1 "/\" z1 );

A6: dom g = NAT by FUNCT_2:def 1;

then reconsider AA = rng g as non empty Subset of L by RELAT_1:42;

A7: AA is GeneratorSet of F by A4, A5, Th32;

A8: F c= G

for x being Element of V1 ex y being Element of V1 st S_{1}[n,x,y]

A17: h . 0 = v1 and

A18: for n being Nat holds S_{1}[n,h . n,h . (n + 1)]
from RECDEF_1:sch 2(A13);

A19: dom h = NAT by FUNCT_2:def 1;

then A20: h . 0 in rng h by FUNCT_1:def 3;

then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;

set O = uparrow (fininfs R);

A21: R c= uparrow (fininfs R) by WAYBEL_0:62;

A22: for x, y being Element of L

for n being Nat st h . n = x & h . (n + 1) = y holds

y <= x

for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds

y <= x

y <= x

for a, b being Element of L st a = g . n & b = g . (n + 1) holds

b <= a

R is_coarser_than O by A21, Th16;

then A73: AA c= O by A65, YELLOW_4:7, YELLOW_4:8;

take O ; :: thesis: ( O c= V & v in O & F c= O )

thus O c= V :: thesis: ( v in O & F c= O )

uparrow (fininfs AA) = F by A7, Def3;

hence F c= O by A73, WAYBEL_0:62; :: thesis: verum

for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let V be upper Open Subset of L; :: thesis: for F being Filter of L

for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let F be Filter of L; :: thesis: for v being Element of L st V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable holds

ex O being Open Filter of L st

( O c= V & v in O & F c= O )

let v be Element of L; :: thesis: ( V "/\" F c= V & v in V & ex A being non empty GeneratorSet of F st A is countable implies ex O being Open Filter of L st

( O c= V & v in O & F c= O ) )

assume that

A1: V "/\" F c= V and

A2: v in V ; :: thesis: ( for A being non empty GeneratorSet of F holds not A is countable or ex O being Open Filter of L st

( O c= V & v in O & F c= O ) )

reconsider V1 = V as non empty upper Open Subset of L by A2;

reconsider v1 = v as Element of V1 by A2;

reconsider G = { x where x is Element of L : V "/\" {x} c= V } as Filter of L by Th23, Th24, Th25;

given A being non empty GeneratorSet of F such that A3: A is countable ; :: thesis: ex O being Open Filter of L st

( O c= V & v in O & F c= O )

consider f being sequence of A such that

A4: rng f = A by A3, CARD_3:96;

reconsider f = f as sequence of the carrier of L by FUNCT_2:7;

deffunc H

consider g being sequence of the carrier of L such that

A5: for n being Element of NAT holds g . n = H

defpred S

( x1 = $2 & y1 = $3 & z1 = g . ($1 + 1) & y1 << x1 "/\" z1 );

A6: dom g = NAT by FUNCT_2:def 1;

then reconsider AA = rng g as non empty Subset of L by RELAT_1:42;

A7: AA is GeneratorSet of F by A4, A5, Th32;

A8: F c= G

proof

A13:
for n being Nat
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F or q in G )

assume A9: q in F ; :: thesis: q in G

then reconsider s = q as Element of L ;

A10: V "/\" {s} = { (s "/\" t) where t is Element of L : t in V } by YELLOW_4:42;

V "/\" {s} c= V

end;assume A9: q in F ; :: thesis: q in G

then reconsider s = q as Element of L ;

A10: V "/\" {s} = { (s "/\" t) where t is Element of L : t in V } by YELLOW_4:42;

V "/\" {s} c= V

proof

hence
q in G
; :: thesis: verum
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in V "/\" {s} or w in V )

assume w in V "/\" {s} ; :: thesis: w in V

then consider t being Element of L such that

A11: w = s "/\" t and

A12: t in V by A10;

t "/\" s in V "/\" F by A9, A12;

hence w in V by A1, A11; :: thesis: verum

end;assume w in V "/\" {s} ; :: thesis: w in V

then consider t being Element of L such that

A11: w = s "/\" t and

A12: t in V by A10;

t "/\" s in V "/\" F by A9, A12;

hence w in V by A1, A11; :: thesis: verum

for x being Element of V1 ex y being Element of V1 st S

proof

consider h being sequence of V1 such that
let n be Nat; :: thesis: for x being Element of V1 ex y being Element of V1 st S_{1}[n,x,y]

let x be Element of V1; :: thesis: ex y being Element of V1 st S_{1}[n,x,y]

AA c= F by A7, Lm4;

then A14: AA c= G by A8;

g . (n + 1) in AA by A6, FUNCT_1:def 3;

then g . (n + 1) in G by A14;

then consider g1 being Element of L such that

A15: g . (n + 1) = g1 and

A16: V "/\" {g1} c= V ;

g1 in {g1} by TARSKI:def 1;

then x "/\" g1 in V "/\" {g1} ;

then ex y1 being Element of L st

( y1 in V & y1 << x "/\" g1 ) by A16, WAYBEL_6:def 1;

hence ex y being Element of V1 st S_{1}[n,x,y]
by A15; :: thesis: verum

end;let x be Element of V1; :: thesis: ex y being Element of V1 st S

AA c= F by A7, Lm4;

then A14: AA c= G by A8;

g . (n + 1) in AA by A6, FUNCT_1:def 3;

then g . (n + 1) in G by A14;

then consider g1 being Element of L such that

A15: g . (n + 1) = g1 and

A16: V "/\" {g1} c= V ;

g1 in {g1} by TARSKI:def 1;

then x "/\" g1 in V "/\" {g1} ;

then ex y1 being Element of L st

( y1 in V & y1 << x "/\" g1 ) by A16, WAYBEL_6:def 1;

hence ex y being Element of V1 st S

A17: h . 0 = v1 and

A18: for n being Nat holds S

A19: dom h = NAT by FUNCT_2:def 1;

then A20: h . 0 in rng h by FUNCT_1:def 3;

then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;

set O = uparrow (fininfs R);

A21: R c= uparrow (fininfs R) by WAYBEL_0:62;

A22: for x, y being Element of L

for n being Nat st h . n = x & h . (n + 1) = y holds

y <= x

proof

A27:
for x, y being Element of L
let x, y be Element of L; :: thesis: for n being Nat st h . n = x & h . (n + 1) = y holds

y <= x

let n be Nat; :: thesis: ( h . n = x & h . (n + 1) = y implies y <= x )

assume A23: ( h . n = x & h . (n + 1) = y ) ; :: thesis: y <= x

consider x1, y1 being Element of V1, z1 being Element of L such that

A24: ( x1 = h . n & y1 = h . (n + 1) ) and

z1 = g . (n + 1) and

A25: y1 << x1 "/\" z1 by A18;

A26: x1 "/\" z1 <= x1 by YELLOW_0:23;

y1 <= x1 "/\" z1 by A25, WAYBEL_3:1;

hence y <= x by A23, A24, A26, ORDERS_2:3; :: thesis: verum

end;y <= x

let n be Nat; :: thesis: ( h . n = x & h . (n + 1) = y implies y <= x )

assume A23: ( h . n = x & h . (n + 1) = y ) ; :: thesis: y <= x

consider x1, y1 being Element of V1, z1 being Element of L such that

A24: ( x1 = h . n & y1 = h . (n + 1) ) and

z1 = g . (n + 1) and

A25: y1 << x1 "/\" z1 by A18;

A26: x1 "/\" z1 <= x1 by YELLOW_0:23;

y1 <= x1 "/\" z1 by A25, WAYBEL_3:1;

hence y <= x by A23, A24, A26, ORDERS_2:3; :: thesis: verum

for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds

y <= x

proof

A36:
for x, y being Element of L st x in R & y in R & not x <= y holds
defpred S_{2}[ Nat] means for a being Element of NAT

for s, t being Element of L st t = h . a & s = h . $1 & a <= $1 holds

s <= t;

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

S_{2}[k + 1]
_{2}[ 0 ]
by NAT_1:3;

A35: for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A34, A28);

let x, y be Element of L; :: thesis: for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds

y <= x

let n, m be Element of NAT ; :: thesis: ( h . n = x & h . m = y & n <= m implies y <= x )

assume ( h . n = x & h . m = y & n <= m ) ; :: thesis: y <= x

hence y <= x by A35; :: thesis: verum

end;for s, t being Element of L st t = h . a & s = h . $1 & a <= $1 holds

s <= t;

A28: for k being Nat st S

S

proof

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

assume A29: for j being Element of NAT

for s, t being Element of L st t = h . j & s = h . k & j <= k holds

s <= t ; :: thesis: S_{2}[k + 1]

k in NAT by ORDINAL1:def 12;

then h . k in R by A19, FUNCT_1:def 3;

then reconsider s = h . k as Element of L ;

let a be Element of NAT ; :: thesis: for s, t being Element of L st t = h . a & s = h . (k + 1) & a <= k + 1 holds

s <= t

let c, d be Element of L; :: thesis: ( d = h . a & c = h . (k + 1) & a <= k + 1 implies c <= d )

assume that

A30: d = h . a and

A31: c = h . (k + 1) and

A32: a <= k + 1 ; :: thesis: c <= d

A33: c <= s by A22, A31;

end;assume A29: for j being Element of NAT

for s, t being Element of L st t = h . j & s = h . k & j <= k holds

s <= t ; :: thesis: S

k in NAT by ORDINAL1:def 12;

then h . k in R by A19, FUNCT_1:def 3;

then reconsider s = h . k as Element of L ;

let a be Element of NAT ; :: thesis: for s, t being Element of L st t = h . a & s = h . (k + 1) & a <= k + 1 holds

s <= t

let c, d be Element of L; :: thesis: ( d = h . a & c = h . (k + 1) & a <= k + 1 implies c <= d )

assume that

A30: d = h . a and

A31: c = h . (k + 1) and

A32: a <= k + 1 ; :: thesis: c <= d

A33: c <= s by A22, A31;

A35: for k being Nat holds S

let x, y be Element of L; :: thesis: for n, m being Element of NAT st h . n = x & h . m = y & n <= m holds

y <= x

let n, m be Element of NAT ; :: thesis: ( h . n = x & h . m = y & n <= m implies y <= x )

assume ( h . n = x & h . m = y & n <= m ) ; :: thesis: y <= x

hence y <= x by A35; :: thesis: verum

y <= x

proof

A43:
uparrow (fininfs R) is Open
let x, y be Element of L; :: thesis: ( x in R & y in R & not x <= y implies y <= x )

assume that

A37: x in R and

A38: y in R ; :: thesis: ( x <= y or y <= x )

consider m being object such that

A39: m in dom h and

A40: y = h . m by A38, FUNCT_1:def 3;

reconsider m = m as Element of NAT by A39;

consider n being object such that

A41: n in dom h and

A42: x = h . n by A37, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A41;

end;assume that

A37: x in R and

A38: y in R ; :: thesis: ( x <= y or y <= x )

consider m being object such that

A39: m in dom h and

A40: y = h . m by A38, FUNCT_1:def 3;

reconsider m = m as Element of NAT by A39;

consider n being object such that

A41: n in dom h and

A42: x = h . n by A37, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A41;

proof

A59:
for n being Element of NAT
let x be Element of L; :: according to WAYBEL_6:def 1 :: thesis: ( not x in uparrow (fininfs R) or ex b_{1} being Element of the carrier of L st

( b_{1} in uparrow (fininfs R) & b_{1} is_way_below x ) )

assume x in uparrow (fininfs R) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in uparrow (fininfs R) & b_{1} is_way_below x )

then consider y being Element of L such that

A44: y <= x and

A45: y in fininfs R by WAYBEL_0:def 16;

consider Y being finite Subset of R such that

A46: y = "/\" (Y,L) and

ex_inf_of Y,L by A45;

end;( b

assume x in uparrow (fininfs R) ; :: thesis: ex b

( b

then consider y being Element of L such that

A44: y <= x and

A45: y in fininfs R by WAYBEL_0:def 16;

consider Y being finite Subset of R such that

A46: y = "/\" (Y,L) and

ex_inf_of Y,L by A45;

per cases
( Y <> {} or Y = {} )
;

end;

suppose
Y <> {}
; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in uparrow (fininfs R) & b_{1} is_way_below x )

( b

then
y in Y
by A36, A46, Th27;

then consider n being object such that

A47: n in dom h and

A48: h . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A47;

consider x1, y1 being Element of V1, z1 being Element of L such that

A49: x1 = h . n and

A50: y1 = h . (n + 1) and

z1 = g . (n + 1) and

A51: y1 << x1 "/\" z1 by A18;

take y1 ; :: thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )

y1 in R by A19, A50, FUNCT_1:def 3;

hence y1 in uparrow (fininfs R) by A21; :: thesis: y1 is_way_below x

x1 "/\" z1 <= x1 by YELLOW_0:23;

then y1 << x1 by A51, WAYBEL_3:2;

hence y1 is_way_below x by A44, A48, A49, WAYBEL_3:2; :: thesis: verum

end;then consider n being object such that

A47: n in dom h and

A48: h . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A47;

consider x1, y1 being Element of V1, z1 being Element of L such that

A49: x1 = h . n and

A50: y1 = h . (n + 1) and

z1 = g . (n + 1) and

A51: y1 << x1 "/\" z1 by A18;

take y1 ; :: thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )

y1 in R by A19, A50, FUNCT_1:def 3;

hence y1 in uparrow (fininfs R) by A21; :: thesis: y1 is_way_below x

x1 "/\" z1 <= x1 by YELLOW_0:23;

then y1 << x1 by A51, WAYBEL_3:2;

hence y1 is_way_below x by A44, A48, A49, WAYBEL_3:2; :: thesis: verum

suppose A52:
Y = {}
; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in uparrow (fininfs R) & b_{1} is_way_below x )

( b

consider b being object such that

A53: b in R by XBOOLE_0:def 1;

reconsider b = b as Element of L by A53;

consider n being object such that

A54: n in dom h and

h . n = b by A53, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A54;

A55: x <= Top L by YELLOW_0:45;

consider x1, y1 being Element of V1, z1 being Element of L such that

x1 = h . n and

A56: y1 = h . (n + 1) and

z1 = g . (n + 1) and

A57: y1 << x1 "/\" z1 by A18;

y = Top L by A46, A52, YELLOW_0:def 12;

then x = Top L by A44, A55, ORDERS_2:2;

then A58: x1 <= x by YELLOW_0:45;

take y1 ; :: thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )

y1 in R by A19, A56, FUNCT_1:def 3;

hence y1 in uparrow (fininfs R) by A21; :: thesis: y1 is_way_below x

x1 "/\" z1 <= x1 by YELLOW_0:23;

then y1 << x1 by A57, WAYBEL_3:2;

hence y1 is_way_below x by A58, WAYBEL_3:2; :: thesis: verum

end;A53: b in R by XBOOLE_0:def 1;

reconsider b = b as Element of L by A53;

consider n being object such that

A54: n in dom h and

h . n = b by A53, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A54;

A55: x <= Top L by YELLOW_0:45;

consider x1, y1 being Element of V1, z1 being Element of L such that

x1 = h . n and

A56: y1 = h . (n + 1) and

z1 = g . (n + 1) and

A57: y1 << x1 "/\" z1 by A18;

y = Top L by A46, A52, YELLOW_0:def 12;

then x = Top L by A44, A55, ORDERS_2:2;

then A58: x1 <= x by YELLOW_0:45;

take y1 ; :: thesis: ( y1 in uparrow (fininfs R) & y1 is_way_below x )

y1 in R by A19, A56, FUNCT_1:def 3;

hence y1 in uparrow (fininfs R) by A21; :: thesis: y1 is_way_below x

x1 "/\" z1 <= x1 by YELLOW_0:23;

then y1 << x1 by A57, WAYBEL_3:2;

hence y1 is_way_below x by A58, WAYBEL_3:2; :: thesis: verum

for a, b being Element of L st a = g . n & b = g . (n + 1) holds

b <= a

proof

A65:
AA is_coarser_than R
let n be Element of NAT ; :: thesis: for a, b being Element of L st a = g . n & b = g . (n + 1) holds

b <= a

let a, b be Element of L; :: thesis: ( a = g . n & b = g . (n + 1) implies b <= a )

assume A60: ( a = g . n & b = g . (n + 1) ) ; :: thesis: b <= a

reconsider gn = { (f . m) where m is Element of NAT : m <= n } , gn1 = { (f . k) where k is Element of NAT : k <= n + 1 } as non empty finite Subset of L by Lm1;

A61: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55;

A62: gn c= gn1

hence b <= a by A61, A62, YELLOW_0:35; :: thesis: verum

end;b <= a

let a, b be Element of L; :: thesis: ( a = g . n & b = g . (n + 1) implies b <= a )

assume A60: ( a = g . n & b = g . (n + 1) ) ; :: thesis: b <= a

reconsider gn = { (f . m) where m is Element of NAT : m <= n } , gn1 = { (f . k) where k is Element of NAT : k <= n + 1 } as non empty finite Subset of L by Lm1;

A61: ( ex_inf_of gn,L & ex_inf_of gn1,L ) by YELLOW_0:55;

A62: gn c= gn1

proof

( a = "/\" (gn,L) & b = "/\" (gn1,L) )
by A5, A60;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in gn or i in gn1 )

assume i in gn ; :: thesis: i in gn1

then consider k being Element of NAT such that

A63: i = f . k and

A64: k <= n ;

k <= n + 1 by A64, NAT_1:12;

hence i in gn1 by A63; :: thesis: verum

end;assume i in gn ; :: thesis: i in gn1

then consider k being Element of NAT such that

A63: i = f . k and

A64: k <= n ;

k <= n + 1 by A64, NAT_1:12;

hence i in gn1 by A63; :: thesis: verum

hence b <= a by A61, A62, YELLOW_0:35; :: thesis: verum

proof

reconsider O = uparrow (fininfs R) as Open Filter of L by A43;
let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in AA or ex b_{1} being Element of the carrier of L st

( b_{1} in R & b_{1} <= a ) )

assume a in AA ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in R & b_{1} <= a )

then consider x being object such that

A66: x in dom g and

A67: g . x = a by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A66;

consider x1, y1 being Element of V1, z1 being Element of L such that

x1 = h . x and

A68: y1 = h . (x + 1) and

A69: z1 = g . (x + 1) and

A70: y1 << x1 "/\" z1 by A18;

( x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 ) by A70, WAYBEL_3:1, YELLOW_0:23;

then A71: y1 <= z1 by ORDERS_2:3;

A72: h . (x + 1) in R by A19, FUNCT_1:def 3;

z1 <= a by A59, A67, A69;

hence ex b being Element of L st

( b in R & b <= a ) by A68, A72, A71, ORDERS_2:3; :: thesis: verum

end;( b

assume a in AA ; :: thesis: ex b

( b

then consider x being object such that

A66: x in dom g and

A67: g . x = a by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A66;

consider x1, y1 being Element of V1, z1 being Element of L such that

x1 = h . x and

A68: y1 = h . (x + 1) and

A69: z1 = g . (x + 1) and

A70: y1 << x1 "/\" z1 by A18;

( x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 ) by A70, WAYBEL_3:1, YELLOW_0:23;

then A71: y1 <= z1 by ORDERS_2:3;

A72: h . (x + 1) in R by A19, FUNCT_1:def 3;

z1 <= a by A59, A67, A69;

hence ex b being Element of L st

( b in R & b <= a ) by A68, A72, A71, ORDERS_2:3; :: thesis: verum

R is_coarser_than O by A21, Th16;

then A73: AA c= O by A65, YELLOW_4:7, YELLOW_4:8;

take O ; :: thesis: ( O c= V & v in O & F c= O )

thus O c= V :: thesis: ( v in O & F c= O )

proof

thus
v in O
by A17, A20, A21; :: thesis: F c= O
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in O or q in V )

assume q in O ; :: thesis: q in V

then reconsider q = q as Element of O ;

consider y being Element of L such that

A74: y <= q and

A75: y in fininfs R by WAYBEL_0:def 16;

consider Y being finite Subset of R such that

A76: y = "/\" (Y,L) and

ex_inf_of Y,L by A75;

end;assume q in O ; :: thesis: q in V

then reconsider q = q as Element of O ;

consider y being Element of L such that

A74: y <= q and

A75: y in fininfs R by WAYBEL_0:def 16;

consider Y being finite Subset of R such that

A76: y = "/\" (Y,L) and

ex_inf_of Y,L by A75;

per cases
( Y <> {} or Y = {} )
;

end;

suppose
Y <> {}
; :: thesis: q in V

then
y in Y
by A36, A76, Th27;

then consider n being object such that

A77: n in dom h and

A78: h . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A77;

ex x1, y1 being Element of V1 ex z1 being Element of L st

( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A18;

hence q in V by A74, A78, WAYBEL_0:def 20; :: thesis: verum

end;then consider n being object such that

A77: n in dom h and

A78: h . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A77;

ex x1, y1 being Element of V1 ex z1 being Element of L st

( x1 = h . n & y1 = h . (n + 1) & z1 = g . (n + 1) & y1 << x1 "/\" z1 ) by A18;

hence q in V by A74, A78, WAYBEL_0:def 20; :: thesis: verum

uparrow (fininfs AA) = F by A7, Def3;

hence F c= O by A73, WAYBEL_0:62; :: thesis: verum