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
reconsider L' = L as complete LATTICE ;
let S be CLSubFrame of L; :: thesis: S is continuous LATTICE
A2:
S is complete LATTICE
by YELLOW_2:32;
for J being non empty set
for K being V9() ManySortedSet of
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
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 ;
:: 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
then reconsider F' =
F as
DoubleIndexedSet of
K,
L by PBOOLE:def 18;
for
j being
Element of
J holds
rng (F' . j) is
directed
then A7:
Inf = Sup
by A1, Lm8;
A8:
ex_inf_of rng (Sups ),
L'
by YELLOW_0:17;
then A12:
rng (Sups ) c= rng (Sups )
by TARSKI:def 3;
then
rng (Sups ) c= rng (Sups )
by TARSKI:def 3;
then A16:
rng (Sups ) = rng (Sups )
by A12, XBOOLE_0:def 10;
ex_inf_of rng (Sups ),
L
by YELLOW_0:17;
then
"/\" (rng (Sups )),
L in the
carrier of
S
by YELLOW_0:def 18;
then
inf (rng (Sups )) = inf (rng (Sups ))
by A8, A16, YELLOW_0:64;
then A17:
Inf = inf (rng (Sups ))
by YELLOW_2:def 6;
A18:
ex_sup_of rng (/\\ (Frege F'),L),
L'
by YELLOW_0:17;
A19:
rng (Infs ) is non
empty directed Subset of
S
by A2, A3, Th27;
now let x be
set ;
:: thesis: ( x in rng (/\\ (Frege F'),L) implies x in rng (Infs ) )assume
x in rng (/\\ (Frege F'),L)
;
:: thesis: x in rng (Infs )then consider f being
set such that A20:
f in dom (Frege F')
and A21:
x = //\ ((Frege F') . f),
L
by Th13;
reconsider f =
f as
Element of
product (doms F') by A20, Lm7;
(Frege F) . f is
Function of
J,the
carrier of
S
by A20, Th10;
then A22:
rng ((Frege F) . f) c= the
carrier of
S
by RELAT_1:def 19;
A23:
ex_inf_of rng ((Frege F) . f),
L'
by YELLOW_0:17;
then A24:
"/\" (rng ((Frege F) . f)),
L in the
carrier of
S
by A22, YELLOW_0:def 18;
x =
"/\" (rng ((Frege F') . f)),
L
by A21, YELLOW_2:def 6
.=
"/\" (rng ((Frege F) . f)),
S
by A22, A23, A24, YELLOW_0:64
.=
//\ ((Frege F) . f),
S
by YELLOW_2:def 6
;
hence
x in rng (Infs )
by A20, Th13;
:: thesis: verum end;
then A25:
rng (/\\ (Frege F'),L) c= rng (/\\ (Frege F),S)
by TARSKI:def 3;
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 A26:
f in dom (Frege F)
and A27:
x = //\ ((Frege F) . f),
S
by Th13;
reconsider f =
f as
Function by A26, Th7;
(Frege F) . f is
Function of
J,the
carrier of
S
by A26, Th10;
then A28:
rng ((Frege F) . f) c= the
carrier of
S
by RELAT_1:def 19;
A29:
ex_inf_of rng ((Frege F) . f),
L'
by YELLOW_0:17;
then A30:
"/\" (rng ((Frege F) . f)),
L in the
carrier of
S
by A28, YELLOW_0:def 18;
x =
"/\" (rng ((Frege F) . f)),
S
by A27, YELLOW_2:def 6
.=
"/\" (rng ((Frege F') . f)),
L
by A28, A29, A30, YELLOW_0:64
.=
//\ ((Frege F') . f),
L
by YELLOW_2:def 6
;
hence
x in rng (Infs )
by A26, Th13;
:: thesis: verum end;
then
rng (Infs ) c= rng (Infs )
by TARSKI:def 3;
then
rng (Infs ) = rng (Infs )
by A25, XBOOLE_0:def 10;
then
sup (rng (Infs )) = sup (rng (Infs ))
by A18, A19, WAYBEL_0:7;
then Sup =
sup (rng (Infs ))
by YELLOW_2:def 5
.=
Sup
by YELLOW_2:def 5
;
hence
Inf = Sup
by A7, A17, YELLOW_2:def 6;
:: thesis: verum
end;
hence
S is continuous LATTICE
by A2, Lm9; :: thesis: verum