let L be complete LATTICE; :: thesis: ( L is continuous implies for S being CLSubFrame of L holds S is continuous LATTICE )

assume A1: L is continuous ; :: thesis: for S being CLSubFrame of L holds S is continuous LATTICE

let S be CLSubFrame of L; :: thesis: S is continuous LATTICE

reconsider L9 = L as complete LATTICE ;

A2: S is complete LATTICE by YELLOW_2:30;

for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

assume A1: L is continuous ; :: thesis: for S being CLSubFrame of L holds S is continuous LATTICE

let S be CLSubFrame of L; :: thesis: S is continuous LATTICE

reconsider L9 = L as complete LATTICE ;

A2: S is complete LATTICE by YELLOW_2:30;

for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

proof

hence
S is continuous LATTICE
by A2, Lm9; :: thesis: verum
let J be non empty set ; :: thesis: for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let F be DoubleIndexedSet of K,S; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

assume A3: for j being Element of J holds rng (F . j) is directed ; :: thesis: Inf = Sup

ex_inf_of rng (Sups ),L by YELLOW_0:17;

then A6: "/\" ((rng (Sups )),L) in the carrier of S by YELLOW_0:def 18;

then ( ex_inf_of rng (Sups ),L9 & rng (Sups ) = rng (Sups ) ) by A9, XBOOLE_0:def 10, YELLOW_0:17;

then inf (rng (Sups )) = inf (rng (Sups )) by A6, YELLOW_0:63;

then A12: Inf = inf (rng (Sups )) by YELLOW_2:def 6;

then A24: rng (Infs ) = rng (Infs ) by A18, XBOOLE_0:def 10;

for j being Element of J holds rng (F9 . j) is directed

( ex_sup_of rng (/\\ ((Frege F9),L)),L9 & rng (Infs ) is non empty directed Subset of S ) by A2, A3, Th27, YELLOW_0:17;

then sup (rng (Infs )) = sup (rng (Infs )) by A24, WAYBEL_0:7;

then Sup = sup (rng (Infs )) by YELLOW_2:def 5

.= Sup by YELLOW_2:def 5 ;

hence Inf = Sup by A25, A12, YELLOW_2:def 6; :: thesis: verum

end;for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,S st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let F be DoubleIndexedSet of K,S; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

assume A3: for j being Element of J holds rng (F . j) is directed ; :: thesis: Inf = Sup

now :: thesis: for j being object st j in J holds

F . j is Function of (K . j),((J --> the carrier of L) . j)

then reconsider F9 = F as DoubleIndexedSet of K,L by PBOOLE:def 15;F . j is Function of (K . j),((J --> the carrier of L) . j)

let j be object ; :: thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) )

assume j in J ; :: thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)

then reconsider j9 = j as Element of J ;

A5: ( F . j9 is Function of (K . j9), the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def 13;

thus F . j is Function of (K . j),((J --> the carrier of L) . j) by A5, FUNCT_2:7; :: thesis: verum

end;assume j in J ; :: thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)

then reconsider j9 = j as Element of J ;

A5: ( F . j9 is Function of (K . j9), the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def 13;

thus F . j is Function of (K . j),((J --> the carrier of L) . j) by A5, FUNCT_2:7; :: thesis: verum

ex_inf_of rng (Sups ),L by YELLOW_0:17;

then A6: "/\" ((rng (Sups )),L) in the carrier of S by YELLOW_0:def 18;

now :: thesis: for x being object st x in rng (Sups ) holds

x in rng (Sups )

then A9:
rng (Sups ) c= rng (Sups )
;x in rng (Sups )

let x be object ; :: thesis: ( x in rng (Sups ) implies x in rng (Sups ) )

assume x in rng (Sups ) ; :: thesis: x in rng (Sups )

then consider j being Element of J such that

A7: x = Sup by Th14;

A8: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;

x = sup (rng (F9 . j)) by A7, YELLOW_2:def 5

.= sup (rng (F . j)) by A8, WAYBEL_0:7

.= Sup by YELLOW_2:def 5 ;

hence x in rng (Sups ) by Th14; :: thesis: verum

end;assume x in rng (Sups ) ; :: thesis: x in rng (Sups )

then consider j being Element of J such that

A7: x = Sup by Th14;

A8: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;

x = sup (rng (F9 . j)) by A7, YELLOW_2:def 5

.= sup (rng (F . j)) by A8, WAYBEL_0:7

.= Sup by YELLOW_2:def 5 ;

hence x in rng (Sups ) by Th14; :: thesis: verum

now :: thesis: for x being object st x in rng (Sups ) holds

x in rng (Sups )

then
rng (Sups ) c= rng (Sups )
;x in rng (Sups )

let x be object ; :: thesis: ( x in rng (Sups ) implies x in rng (Sups ) )

assume x in rng (Sups ) ; :: thesis: x in rng (Sups )

then consider j being Element of J such that

A10: x = Sup by Th14;

A11: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;

x = sup (rng (F . j)) by A10, YELLOW_2:def 5

.= sup (rng (F9 . j)) by A11, WAYBEL_0:7

.= Sup by YELLOW_2:def 5 ;

hence x in rng (Sups ) by Th14; :: thesis: verum

end;assume x in rng (Sups ) ; :: thesis: x in rng (Sups )

then consider j being Element of J such that

A10: x = Sup by Th14;

A11: ( ex_sup_of rng (F . j),L9 & rng (F . j) is directed Subset of S ) by A3, YELLOW_0:17;

x = sup (rng (F . j)) by A10, YELLOW_2:def 5

.= sup (rng (F9 . j)) by A11, WAYBEL_0:7

.= Sup by YELLOW_2:def 5 ;

hence x in rng (Sups ) by Th14; :: thesis: verum

then ( ex_inf_of rng (Sups ),L9 & rng (Sups ) = rng (Sups ) ) by A9, XBOOLE_0:def 10, YELLOW_0:17;

then inf (rng (Sups )) = inf (rng (Sups )) by A6, YELLOW_0:63;

then A12: Inf = inf (rng (Sups )) by YELLOW_2:def 6;

now :: thesis: for x being object st x in rng (Infs ) holds

x in rng (Infs )

then A18:
rng (Infs ) c= rng (Infs )
;x in rng (Infs )

let x be object ; :: thesis: ( x in rng (Infs ) implies x in rng (Infs ) )

assume x in rng (Infs ) ; :: thesis: x in rng (Infs )

then consider f being object such that

A13: f in dom (Frege F) and

A14: x = //\ (((Frege F) . f),S) by Th13;

reconsider f = f as Function by A13;

(Frege F) . f is Function of J, the carrier of S by A13, Th10;

then A15: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def 19;

A16: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;

then A17: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A15, YELLOW_0:def 18;

x = "/\" ((rng ((Frege F) . f)),S) by A14, YELLOW_2:def 6

.= "/\" ((rng ((Frege F9) . f)),L) by A15, A16, A17, YELLOW_0:63

.= //\ (((Frege F9) . f),L) by YELLOW_2:def 6 ;

hence x in rng (Infs ) by A13, Th13; :: thesis: verum

end;assume x in rng (Infs ) ; :: thesis: x in rng (Infs )

then consider f being object such that

A13: f in dom (Frege F) and

A14: x = //\ (((Frege F) . f),S) by Th13;

reconsider f = f as Function by A13;

(Frege F) . f is Function of J, the carrier of S by A13, Th10;

then A15: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def 19;

A16: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;

then A17: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A15, YELLOW_0:def 18;

x = "/\" ((rng ((Frege F) . f)),S) by A14, YELLOW_2:def 6

.= "/\" ((rng ((Frege F9) . f)),L) by A15, A16, A17, YELLOW_0:63

.= //\ (((Frege F9) . f),L) by YELLOW_2:def 6 ;

hence x in rng (Infs ) by A13, Th13; :: thesis: verum

now :: thesis: for x being object st x in rng (/\\ ((Frege F9),L)) holds

x in rng (Infs )

then
rng (/\\ ((Frege F9),L)) c= rng (/\\ ((Frege F),S))
;x in rng (Infs )

let x be object ; :: thesis: ( x in rng (/\\ ((Frege F9),L)) implies x in rng (Infs ) )

assume x in rng (/\\ ((Frege F9),L)) ; :: thesis: x in rng (Infs )

then consider f being object such that

A19: f in dom (Frege F9) and

A20: x = //\ (((Frege F9) . f),L) by Th13;

reconsider f = f as Element of product (doms F9) by A19;

(Frege F) . f is Function of J, the carrier of S by A19, Th10;

then A21: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def 19;

A22: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;

then A23: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A21, YELLOW_0:def 18;

x = "/\" ((rng ((Frege F9) . f)),L) by A20, YELLOW_2:def 6

.= "/\" ((rng ((Frege F) . f)),S) by A21, A22, A23, YELLOW_0:63

.= //\ (((Frege F) . f),S) by YELLOW_2:def 6 ;

hence x in rng (Infs ) by A19, Th13; :: thesis: verum

end;assume x in rng (/\\ ((Frege F9),L)) ; :: thesis: x in rng (Infs )

then consider f being object such that

A19: f in dom (Frege F9) and

A20: x = //\ (((Frege F9) . f),L) by Th13;

reconsider f = f as Element of product (doms F9) by A19;

(Frege F) . f is Function of J, the carrier of S by A19, Th10;

then A21: rng ((Frege F) . f) c= the carrier of S by RELAT_1:def 19;

A22: ex_inf_of rng ((Frege F) . f),L9 by YELLOW_0:17;

then A23: "/\" ((rng ((Frege F) . f)),L) in the carrier of S by A21, YELLOW_0:def 18;

x = "/\" ((rng ((Frege F9) . f)),L) by A20, YELLOW_2:def 6

.= "/\" ((rng ((Frege F) . f)),S) by A21, A22, A23, YELLOW_0:63

.= //\ (((Frege F) . f),S) by YELLOW_2:def 6 ;

hence x in rng (Infs ) by A19, Th13; :: thesis: verum

then A24: rng (Infs ) = rng (Infs ) by A18, XBOOLE_0:def 10;

for j being Element of J holds rng (F9 . j) is directed

proof

then A25:
Inf = Sup
by A1, Lm8;
let j be Element of J; :: thesis: rng (F9 . j) is directed

rng (F . j) is directed by A3;

hence rng (F9 . j) is directed by YELLOW_2:7; :: thesis: verum

end;rng (F . j) is directed by A3;

hence rng (F9 . j) is directed by YELLOW_2:7; :: thesis: verum

( ex_sup_of rng (/\\ ((Frege F9),L)),L9 & rng (Infs ) is non empty directed Subset of S ) by A2, A3, Th27, YELLOW_0:17;

then sup (rng (Infs )) = sup (rng (Infs )) by A24, WAYBEL_0:7;

then Sup = sup (rng (Infs )) by YELLOW_2:def 5

.= Sup by YELLOW_2:def 5 ;

hence Inf = Sup by A25, A12, YELLOW_2:def 6; :: thesis: verum