let L be lower-bounded up-complete LATTICE; :: thesis: ( SupMap L is upper_adjoint implies L is continuous )
set P = InclPoset (Ids L);
assume A1: SupMap L is upper_adjoint ; :: thesis: L is continuous
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

set r = SupMap L;
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 I9 = inf ((SupMap L) " (uparrow x));
reconsider I = inf ((SupMap L) " (uparrow x)) as Ideal of L by YELLOW_2:41;
A2: 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 J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;
assume x <= sup J ; :: thesis: I c= J
then x <= (SupMap L) . J9 by YELLOW_2:def 3;
then ( J in dom (SupMap L) & (SupMap L) . J9 in uparrow x ) by WAYBEL_0:18, YELLOW_2:50;
then J9 in (SupMap L) " (uparrow x) by FUNCT_1:def 7;
then inf ((SupMap L) " (uparrow x)) <= J9 by YELLOW_2:22;
hence I c= J by YELLOW_1:3; :: thesis: verum

end;

consider d being Function of L,(InclPoset (Ids L)) such that
A3: [(SupMap L),d] is Galois by A1, WAYBEL_1:def 11;
d . x is_minimum_of (SupMap L) " (uparrow x) by A3, WAYBEL_1:10;
then I in (SupMap L) " (uparrow x) by WAYBEL_1:def 6;
then (SupMap L) . I in uparrow x by FUNCT_1:def 7;
then x <= (SupMap L) . (inf ((SupMap L) " (uparrow x))) by WAYBEL_0:18;
then x <= sup I by YELLOW_2:def 3;
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 A2; :: thesis: verum

end;

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