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 ) )

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

hence
L is continuous
by Lm4; :: thesis: verum
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

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;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

consider d being Function of L,(InclPoset (Ids L)) such that
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;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

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