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

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

now

let j be set ; :: thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) )
assume A4: 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;
(J --> the carrier of L) . j = the carrier of L by A4, FUNCOP_1:13;
hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A5, FUNCT_2:9; :: thesis: verum

end;

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

let x be set ; :: 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 ) by TARSKI:def 3;

now

let x be set ; :: 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 ) by TARSKI:def 3;
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:64;
then A12: Inf = inf (rng (Sups )) by YELLOW_2:def 6;

now

let x be set ; :: thesis: ( x in rng (Infs ) implies x in rng (Infs ) )
assume x in rng (Infs ) ; :: thesis: x in rng (Infs )
then consider f being set such that
A13: f in dom (Frege F) and
A14: x = //\ ((Frege F) . f),S by Th13;
reconsider f = f as Function by A13, Th7;
(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:64
.= //\ ((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 ) by TARSKI:def 3;

now

let x be set ; :: 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 set 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, Lm7;
(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:64
.= //\ ((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) by TARSKI:def 3;
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