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 non-empty 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

let J be non empty set ; :: thesis: for K being non-empty 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 non-empty 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)

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;

then reconsider F9 = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
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 )

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;

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

now :: thesis: for x being object st x in rng (Sups ) holds
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;

then rng (Sups ) c= rng (Sups ) ;
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 )

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;

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

now :: thesis: for x being object st x in rng (/\\ ((Frege F9),L)) holds
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;

then rng (/\\ ((Frege F9),L)) c= rng (/\\ ((Frege F),S)) ;
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

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;

then A25: Inf = Sup by A1, Lm8;
( 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;

hence S is continuous LATTICE by A2, Lm9; :: thesis: verum