let L be complete LATTICE; :: thesis:

hereby :: thesis:

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

end;

assume A2: L is meet-continuous ; :: thesis:
given R being auxiliary approximating Relation of L such that A3: for R9 being auxiliary approximating Relation of L holds R c= R9 ; :: thesis:
for x being Element of L holds x = sup (waybelow x)

proof

let x be Element of L; :: thesis:
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:
assume a in { (AR -below x) where AR is auxiliary Relation of L : AR in App L } ; :: thesis:
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:
assume A10: b in R -below x ; :: thesis:
R -below x c= AA -below x by A3, Th29;
hence b in a by A8, A10; :: thesis:

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:

end;

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