let L be complete LATTICE; :: thesis: ( L is continuous implies for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE )

assume A1: L is continuous ; :: thesis: for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE

let S be non empty Poset; :: thesis: ( ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE )

given g being Function of L,S such that A2: ( g is infs-preserving & g is directed-sups-preserving ) and
A3: g is onto ; :: thesis:
reconsider S9 = S as complete LATTICE by A2, A3, Th29;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S9 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,S9 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,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup

let F be DoubleIndexedSet of K,S9; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A4: for j being Element of J holds rng (F . j) is directed ; :: thesis:
consider d being Function of S,L such that
A5: [g,d] is Galois and
for t being Element of S holds d . t is_minimum_of g " () by ;
reconsider dF = (J => d) ** F as DoubleIndexedSet of K,L by Th31;
A6: ( ex_inf_of rng (),L & g preserves_inf_of rng () ) by ;
for t being Element of S holds d . t is_minimum_of g " {t} by ;
then A7: g * d = id S by WAYBEL_1:23;
A8: for f being set st f in dom (Frege dF) holds
rng (() . f) = g .: (rng ((Frege dF) . f))
proof
let f be set ; :: thesis: ( f in dom (Frege dF) implies rng (() . f) = g .: (rng ((Frege dF) . f)) )
assume A9: f in dom (Frege dF) ; :: thesis: rng (() . f) = g .: (rng ((Frege dF) . f))
then reconsider f = f as Element of product (doms dF) ;
A10: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2
.= product (doms F) by Th32
.= dom () by PARTFUN1:def 2 ;
A11: dom ((Frege dF) . f) = dom dF by
.= J by PARTFUN1:def 2 ;
A12: now :: thesis: for i being object st i in J holds
(g * ((Frege dF) . f)) . i = (() . f) . i
let i be object ; :: thesis: ( i in J implies (g * ((Frege dF) . f)) . i = (() . f) . i )
assume A13: i in J ; :: thesis: (g * ((Frege dF) . f)) . i = (() . f) . i
then reconsider j = i as Element of J ;
A14: j in dom F by ;
A15: j in dom dF by ;
then f . j in dom (dF . j) by ;
then f . j in dom (((J => d) . j) * (F . j)) by MSUALG_3:2;
then A16: f . j in dom (d * (F . j)) ;
(g * ((Frege dF) . f)) . j = g . (((Frege dF) . f) . j) by
.= g . ((dF . j) . (f . j)) by A9, A15, Th9
.= g . ((((J => d) . j) * (F . j)) . (f . j)) by MSUALG_3:2
.= g . ((d * (F . j)) . (f . j))
.= (g * (d * (F . j))) . (f . j) by
.= ((id the carrier of S) * (F . j)) . (f . j) by
.= (F . j) . (f . j) by FUNCT_2:17
.= (() . f) . j by A9, A10, A14, Th9 ;
hence (g * ((Frege dF) . f)) . i = (() . f) . i ; :: thesis: verum
end;
dom g = the carrier of L by FUNCT_2:def 1;
then rng ((Frege dF) . f) c= dom g ;
then A17: dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f) by RELAT_1:27;
dom (() . f) = dom F by A9, A10, Th8
.= J by PARTFUN1:def 2 ;
then rng (() . f) = rng (g * ((Frege dF) . f)) by
.= g .: (rng ((Frege dF) . f)) by RELAT_1:127 ;
hence rng (() . f) = g .: (rng ((Frege dF) . f)) ; :: thesis: verum
end;
A18: rng () c= g .: (rng ())
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng () or y in g .: (rng ()) )
assume y in rng () ; :: thesis: y in g .: (rng ())
then consider f being object such that
A19: f in dom () and
A20: y = //\ ((() . f),S) by Th13;
reconsider f = f as Element of product (doms F) by A19;
reconsider f9 = f as Element of product (doms dF) by Th32;
set X = rng ((Frege dF) . f9);
A21: ( g preserves_inf_of rng ((Frege dF) . f9) & ex_inf_of rng ((Frege dF) . f9),L ) by ;
A22: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2
.= product (doms F) by Th32
.= dom () by PARTFUN1:def 2 ;
then rng (() . f) = g .: (rng ((Frege dF) . f)) by ;
then y = "/\" ((g .: (rng ((Frege dF) . f))),S) by ;
then A23: y = g . (inf (rng ((Frege dF) . f9))) by
.= g . () by YELLOW_2:def 6 ;
Inf in rng () by ;
hence y in g .: (rng ()) by ; :: thesis: verum
end;
A24: g .: (rng ()) c= rng ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: (rng ()) or y in rng () )
assume y in g .: (rng ()) ; :: thesis: y in rng ()
then consider x being object such that
x in the carrier of L and
A25: x in rng () and
A26: y = g . x by FUNCT_2:64;
consider f being object such that
A27: f in dom (Frege dF) and
A28: x = //\ (((Frege dF) . f),L) by ;
reconsider f = f as Element of product (doms dF) by A27;
set X = rng ((Frege dF) . f);
( g preserves_inf_of rng ((Frege dF) . f) & ex_inf_of rng ((Frege dF) . f),L ) by ;
then inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f))) by WAYBEL_0:def 30;
then A29: y = inf (g .: (rng ((Frege dF) . f))) by ;
A30: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2
.= product (doms F) by Th32
.= dom () by PARTFUN1:def 2 ;
reconsider f9 = f as Element of product (doms F) by Th32;
rng (() . f) = g .: (rng ((Frege dF) . f)) by ;
then y = Inf by ;
hence y in rng () by ; :: thesis: verum
end;
A31: d is monotone by ;
A32: for j being Element of J holds rng (dF . j) is directed
proof
let j be Element of J; :: thesis: rng (dF . j) is directed
(J => d) . j = d ;
then A33: rng (dF . j) = rng (d * (F . j)) by MSUALG_3:2
.= d .: (rng (F . j)) by RELAT_1:127 ;
rng (F . j) is directed by A4;
hence rng (dF . j) is directed by ; :: thesis: verum
end;
then ( rng () is directed & not rng () is empty ) by Th27;
then A34: g preserves_sup_of rng () by ;
reconsider gdF = (J => g) ** dF as DoubleIndexedSet of K,S ;
A35: ex_sup_of rng (),L by YELLOW_0:17;
A36: rng () c= g .: (rng ())
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng () or y in g .: (rng ()) )
assume y in rng () ; :: thesis: y in g .: (rng ())
then consider j being Element of J such that
A37: y = Sup by Th14;
gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2
.= g * (dF . j) ;
then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;
then A38: y = sup (g .: (rng (dF . j))) by ;
rng (dF . j) is directed by A32;
then A39: g preserves_sup_of rng (dF . j) by ;
ex_sup_of rng (dF . j),L by YELLOW_0:17;
then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by ;
then A40: y = g . () by ;
Sup in rng () by Th14;
hence y in g .: (rng ()) by ; :: thesis: verum
end;
A41: g .: (rng ()) c= rng ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: (rng ()) or y in rng () )
assume y in g .: (rng ()) ; :: thesis: y in rng ()
then consider x being object such that
x in the carrier of L and
A42: x in rng () and
A43: y = g . x by FUNCT_2:64;
consider j being Element of J such that
A44: x = Sup by ;
rng (dF . j) is directed by A32;
then A45: g preserves_sup_of rng (dF . j) by ;
ex_sup_of rng (dF . j),L by YELLOW_0:17;
then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by ;
then A46: y = sup (g .: (rng (dF . j))) by ;
gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2
.= g * (dF . j) ;
then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;
then y = Sup by ;
hence y in rng () by Th14; :: thesis: verum
end;
F = (id (J --> the carrier of S)) ** F by MSUALG_3:4
.= ((J --> g) ** (J --> d)) ** F by
.= gdF by PBOOLE:140 ;
then Inf = inf (rng ()) by YELLOW_2:def 6
.= inf (g .: (rng ())) by
.= g . (inf (rng ())) by
.= g . () by YELLOW_2:def 6
.= g . () by A1, A32, Lm8
.= g . (sup (rng ())) by YELLOW_2:def 5
.= sup (g .: (rng ())) by
.= sup (rng ()) by
.= Sup by YELLOW_2:def 5 ;
hence Inf = Sup ; :: thesis: verum
end;
hence S is continuous LATTICE by Lm9; :: thesis: verum