let L be complete LATTICE; ( L is continuous iff for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) )
set AR = L -waybelow ;
hereby ( ( for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ) implies L is continuous )
assume A1:
L is
continuous
;
for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating )then reconsider L9 =
L as
lower-bounded meet-continuous LATTICE ;
thus
for
R being
auxiliary approximating Relation of
L holds
(
L -waybelow c= R &
L -waybelow is
approximating )
verumproof
let R be
auxiliary approximating Relation of
L;
( L -waybelow c= R & L -waybelow is approximating )
reconsider R9 =
R as
auxiliary approximating Relation of
L9 ;
for
a,
b being
object st
[a,b] in L -waybelow holds
[a,b] in R
proof
let a,
b be
object ;
( [a,b] in L -waybelow implies [a,b] in R )
assume A2:
[a,b] in L -waybelow
;
[a,b] in R
then reconsider a9 =
a,
b9 =
b as
Element of
L9 by ZFMISC_1:87;
a9 << b9
by A2, Def1;
then A3:
a9 in waybelow b9
by WAYBEL_3:7;
A4:
meet { (A1 -below b9) where A1 is auxiliary Relation of L9 : A1 in App L9 } = waybelow b9
by Th44;
R9 in App L9
by Def19;
then
R9 -below b9 in { (A1 -below b9) where A1 is auxiliary Relation of L9 : A1 in App L9 }
;
then
waybelow b9 c= R9 -below b9
by A4, SETFAM_1:3;
hence
[a,b] in R
by A3, Th13;
verum
end;
hence
L -waybelow c= R
;
L -waybelow is approximating
thus
L -waybelow is
approximating
by A1;
verum
end;
end;
assume A5:
for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating )
; L is continuous
for x being Element of L holds x = sup (waybelow x)
then
L is satisfying_axiom_of_approximation
by WAYBEL_3:def 5;
hence
L is continuous
; verum