let L be complete LATTICE; :: thesis: ( L is continuous iff for R being auxiliary approximating Relation of holds
( L -waybelow c= R & L -waybelow is approximating ) )
set AR = L -waybelow ;

hereby :: thesis: ( ( for R being auxiliary approximating Relation of 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 holds
( L -waybelow c= R & L -waybelow is approximating )
then reconsider L' = L as lower-bounded meet-continuous LATTICE ;
thus for R being auxiliary approximating Relation of holds
( L -waybelow c= R & L -waybelow is approximating ) :: thesis: verum

proof

let R be auxiliary approximating Relation of ; :: thesis: ( L -waybelow c= R & L -waybelow is approximating )
reconsider R' = R as auxiliary approximating Relation of ;
for a, b being set st [a,b] in L -waybelow holds
[a,b] in R

proof

let a, b be set ; :: 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 a' = a, b' = b as Element of by ZFMISC_1:106;
a' << b' by A2, Def2;
then A3: a' in waybelow b' by WAYBEL_3:7;
A4: meet { (A1 -below b') where A1 is auxiliary Relation of : A1 in App L' } = waybelow b' by Th44;
R' in App L' by Def20;
then R' -below b' in { (A1 -below b') where A1 is auxiliary Relation of : A1 in App L' } ;
then waybelow b' c= R' -below b' by A4, SETFAM_1:4;
hence [a,b] in R by A3, Th13; :: thesis: verum

end;

hence L -waybelow c= R by RELAT_1:def 3; :: 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 holds
( L -waybelow c= R & L -waybelow is approximating ) ; :: thesis: L is continuous
for x being Element of holds x = sup (waybelow x)

proof

let x be Element of ; :: thesis: x = sup (waybelow x)
x = sup ((L -waybelow ) -below x) by A5, Def18;
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