let L be complete LATTICE; :: thesis: ( 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 :: thesis: ( ( 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 ; :: thesis: 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 ) :: thesis: verum

proof

let R be auxiliary approximating Relation of L; :: thesis: ( 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 ; :: thesis: ( [a,b] in L -waybelow implies [a,b] in R )
assume A2: [a,b] in L -waybelow ; :: thesis: [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; :: thesis: verum

end;

hence L -waybelow c= R ; :: thesis: L -waybelow is approximating
thus L -waybelow is approximating by A1; :: thesis: verum

end;

end;

assume A5: for R being auxiliary approximating Relation of L holds
( L -waybelow c= R & L -waybelow is approximating ) ; :: thesis: L is continuous
for x being Element of L holds x = sup (waybelow x)

proof

let x be Element of L; :: thesis: x = sup (waybelow x)
x = sup ((L -waybelow) -below x) by A5, Def17;
hence x = sup (waybelow x) by Th40; :: thesis: verum

end;

then L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
hence L is continuous ; :: thesis: verum