let L be lower-bounded up-complete LATTICE; :: thesis: ( SupMap L is upper_adjoint implies L is continuous )
assume A1: SupMap L is upper_adjoint ; :: thesis: L is continuous
set P = InclPoset (Ids L);
for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )

proof

let x be Element of L; :: thesis: ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
set r = SupMap L;
set I' = inf ((SupMap L) " (uparrow x));
reconsider I = inf ((SupMap L) " (uparrow x)) as Ideal of L by YELLOW_2:43;
consider d being Function of L,(InclPoset (Ids L)) such that
A2: [(SupMap L),d] is Galois by A1, WAYBEL_1:def 11;
d . x is_minimum_of (SupMap L) " (uparrow x) by A2, WAYBEL_1:11;
then ( ex_inf_of (SupMap L) " (uparrow x), InclPoset (Ids L) & d . x = I & I in (SupMap L) " (uparrow x) ) by WAYBEL_1:def 6;
then (SupMap L) . I in uparrow x by FUNCT_1:def 13;
then x <= (SupMap L) . (inf ((SupMap L) " (uparrow x))) by WAYBEL_0:18;
then A3: x <= sup I by YELLOW_2:def 3;
for J being Ideal of L st x <= sup J holds
I c= J

proof

let J be Ideal of L; :: thesis: ( x <= sup J implies I c= J )
reconsider J' = J as Element of (InclPoset (Ids L)) by YELLOW_2:43;
A4: J in dom (SupMap L) by YELLOW_2:52;
assume x <= sup J ; :: thesis: I c= J
then x <= (SupMap L) . J' by YELLOW_2:def 3;
then (SupMap L) . J' in uparrow x by WAYBEL_0:18;
then J' in (SupMap L) " (uparrow x) by A4, FUNCT_1:def 13;
then inf ((SupMap L) " (uparrow x)) <= J' by YELLOW_2:24;
hence I c= J by YELLOW_1:3; :: thesis: verum

end;

hence ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) by A3; :: thesis: verum

end;

hence L is continuous by Lm4; :: thesis: verum