let L be complete continuous LATTICE; for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]
let R be Subset of [:L,L:]; ( R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) implies subrelstr R is CLSubFrame of [:L,L:] )
assume
R is Equivalence_Relation of the carrier of L
; ( for LR being complete continuous LATTICE holds
( not the carrier of LR = Class (EqRel R) or ex g being Function of L,LR st
( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) & g is not CLHomomorphism of L,LR ) ) or subrelstr R is CLSubFrame of [:L,L:] )
then A1:
EqRel R = R
by Def1;
set ER = EqRel R;
given LR being complete continuous LATTICE such that A2:
the carrier of LR = Class (EqRel R)
and
A3:
for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR
; subrelstr R is CLSubFrame of [:L,L:]
deffunc H1( object ) -> Element of bool the carrier of L = Class ((EqRel R),$1);
set CER = Class (EqRel R);
set cL = the carrier of L;
set cLR = the carrier of LR;
A4:
for x being object st x in the carrier of L holds
H1(x) in Class (EqRel R)
by EQREL_1:def 3;
consider g being Function of the carrier of L,(Class (EqRel R)) such that
A5:
for x being object st x in the carrier of L holds
g . x = H1(x)
from FUNCT_2:sch 2(A4);
reconsider g = g as Function of L,LR by A2;
set k = g;
A6:
dom g = the carrier of L
by FUNCT_2:def 1;
now for x being object holds
( ( x in R implies x in [:g,g:] " (id the carrier of LR) ) & ( x in [:g,g:] " (id the carrier of LR) implies x in R ) )let x be
object ;
( ( x in R implies x in [:g,g:] " (id the carrier of LR) ) & ( x in [:g,g:] " (id the carrier of LR) implies x in R ) )hereby ( x in [:g,g:] " (id the carrier of LR) implies x in R )
assume A7:
x in R
;
x in [:g,g:] " (id the carrier of LR)then
x in the
carrier of
[:L,L:]
;
then
x in [: the carrier of L, the carrier of L:]
by YELLOW_3:def 2;
then consider x1,
x2 being
object such that A8:
(
x1 in the
carrier of
L &
x2 in the
carrier of
L )
and A9:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
L by A8;
A10:
(
g . x1 = Class (
(EqRel R),
x1) &
g . x2 = Class (
(EqRel R),
x2) )
by A5;
x1 in Class (
(EqRel R),
x2)
by A1, A7, A9, EQREL_1:19;
then
g . x1 = g . x2
by A10, EQREL_1:23;
then A11:
[(g . x1),(g . x2)] in id the
carrier of
LR
by RELAT_1:def 10;
dom [:g,g:] = [:(dom g),(dom g):]
by FUNCT_3:def 8;
then A12:
[x1,x2] in dom [:g,g:]
by A6, ZFMISC_1:87;
[:g,g:] . (
x1,
x2)
= [(g . x1),(g . x2)]
by A6, FUNCT_3:def 8;
hence
x in [:g,g:] " (id the carrier of LR)
by A9, A11, A12, FUNCT_1:def 7;
verum
end; assume A13:
x in [:g,g:] " (id the carrier of LR)
;
x in Rthen A14:
[:g,g:] . x in id the
carrier of
LR
by FUNCT_1:def 7;
x in dom [:g,g:]
by A13, FUNCT_1:def 7;
then
x in [:(dom g),(dom g):]
by FUNCT_3:def 8;
then consider x1,
x2 being
object such that A15:
(
x1 in dom g &
x2 in dom g )
and A16:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Element of
L by A15;
A17:
(
g . x1 = Class (
(EqRel R),
x1) &
g . x2 = Class (
(EqRel R),
x2) )
by A5;
[:g,g:] . (
x1,
x2)
= [(g . x1),(g . x2)]
by A15, FUNCT_3:def 8;
then
g . x1 = g . x2
by A14, A16, RELAT_1:def 10;
then
x1 in Class (
(EqRel R),
x2)
by A17, EQREL_1:23;
hence
x in R
by A1, A16, EQREL_1:19;
verum end;
then A18:
R = [:g,g:] " (id the carrier of LR)
by TARSKI:2;
for x being Element of L holds g . x = Class ((EqRel R),x)
by A5;
then
g is CLHomomorphism of L,LR
by A3;
hence
subrelstr R is CLSubFrame of [:L,L:]
by A18, Th34; verum