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:
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
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:
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 ; :: thesis: verum
end;
then reconsider F9 = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
ex_inf_of rng (),L by YELLOW_0:17;
then A6: "/\" ((rng ()),L) in the carrier of S by YELLOW_0:def 18;
now :: thesis: for x being object st x in rng () holds
x in rng ()
let x be object ; :: thesis: ( x in rng () implies x in rng () )
assume x in rng () ; :: thesis: x in rng ()
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 ;
x = sup (rng (F9 . j)) by
.= sup (rng (F . j)) by
.= Sup by YELLOW_2:def 5 ;
hence x in rng () by Th14; :: thesis: verum
end;
then A9: rng () c= rng () ;
now :: thesis: for x being object st x in rng () holds
x in rng ()
let x be object ; :: thesis: ( x in rng () implies x in rng () )
assume x in rng () ; :: thesis: x in rng ()
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 ;
x = sup (rng (F . j)) by
.= sup (rng (F9 . j)) by
.= Sup by YELLOW_2:def 5 ;
hence x in rng () by Th14; :: thesis: verum
end;
then rng () c= rng () ;
then ( ex_inf_of rng (),L9 & rng () = rng () ) by ;
then inf (rng ()) = inf (rng ()) by ;
then A12: Inf = inf (rng ()) by YELLOW_2:def 6;
now :: thesis: for x being object st x in rng () holds
x in rng ()
let x be object ; :: thesis: ( x in rng () implies x in rng () )
assume x in rng () ; :: thesis: x in rng ()
then consider f being object such that
A13: f in dom () and
A14: x = //\ ((() . f),S) by Th13;
reconsider f = f as Function by A13;
(Frege F) . f is Function of J, the carrier of S by ;
then A15: rng (() . f) c= the carrier of S by RELAT_1:def 19;
A16: ex_inf_of rng (() . f),L9 by YELLOW_0:17;
then A17: "/\" ((rng (() . f)),L) in the carrier of S by ;
x = "/\" ((rng (() . f)),S) by
.= "/\" ((rng ((Frege F9) . f)),L) by
.= //\ (((Frege F9) . f),L) by YELLOW_2:def 6 ;
hence x in rng () by ; :: thesis: verum
end;
then A18: rng () c= rng () ;
now :: thesis: for x being object st x in rng (/\\ ((Frege F9),L)) holds
x in rng ()
let x be object ; :: thesis: ( x in rng (/\\ ((Frege F9),L)) implies x in rng () )
assume x in rng (/\\ ((Frege F9),L)) ; :: thesis: x in rng ()
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 ;
then A21: rng (() . f) c= the carrier of S by RELAT_1:def 19;
A22: ex_inf_of rng (() . f),L9 by YELLOW_0:17;
then A23: "/\" ((rng (() . f)),L) in the carrier of S by ;
x = "/\" ((rng ((Frege F9) . f)),L) by
.= "/\" ((rng (() . f)),S) by
.= //\ ((() . f),S) by YELLOW_2:def 6 ;
hence x in rng () by ; :: thesis: verum
end;
then rng (/\\ ((Frege F9),L)) c= rng (/\\ ((),S)) ;
then A24: rng () = rng () by ;
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 ;
( ex_sup_of rng (/\\ ((Frege F9),L)),L9 & rng () is non empty directed Subset of S ) by ;
then sup (rng ()) = sup (rng ()) by ;
then Sup = sup (rng ()) by YELLOW_2:def 5
.= Sup by YELLOW_2:def 5 ;
hence Inf = Sup by ; :: thesis: verum
end;
hence S is continuous LATTICE by ; :: thesis: verum