let L be complete LATTICE; :: thesis: ( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 ) )

hereby :: thesis: ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 implies L is continuous )

assume A1: L is continuous ; :: thesis: ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 )
hence L is meet-continuous ; :: thesis: ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9
reconsider R = L -waybelow as auxiliary approximating Relation of L by A1;
take R = R; :: thesis: for R9 being auxiliary approximating Relation of L holds R c= R9
thus for R9 being auxiliary approximating Relation of L holds R c= R9 by A1, Th45; :: thesis: verum

end;

assume A2: L is meet-continuous ; :: thesis: ( for R being auxiliary approximating Relation of L holds
not for R9 being auxiliary approximating Relation of L holds R c= R9 or L is continuous )
given R being auxiliary approximating Relation of L such that A3: for R9 being auxiliary approximating Relation of L holds R c= R9 ; :: 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)
set K = { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ;
A4: meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } = waybelow x by A2, Th44;
R in App L by Def19;
then A5: R -below x in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ;
then A6: waybelow x c= R -below x by A4, SETFAM_1:3;
A7: sup (R -below x) = x by Def17;
for a being set st a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } holds
R -below x c= a

proof

let a be set ; :: thesis: ( a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } implies R -below x c= a )
assume a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ; :: thesis: R -below x c= a
then consider AA being auxiliary Relation of L such that
A8: a = AA -below x and
A9: AA in App L ;
reconsider AA = AA as auxiliary approximating Relation of L by A9, Def19;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in R -below x or b in a )
assume A10: b in R -below x ; :: thesis: b in a
R -below x c= AA -below x by A3, Th29;
hence b in a by A8, A10; :: thesis: verum

end;

then R -below x c= meet { (AR -below x) where AR is auxiliary Relation of L : AR in App L } by A5, SETFAM_1:5;
hence x = sup (waybelow x) by A4, A6, A7, XBOOLE_0:def 10; :: thesis: verum

end;

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