let L be non empty complete Poset; :: thesis: ( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )
set i = (IdsMap L) * (SupMap L);

A1: now :: thesis: for I being Ideal of L holds ((IdsMap L) * (SupMap L)) . I = downarrow (sup I)

let I be Ideal of L; :: thesis: ((IdsMap L) * (SupMap L)) . I = downarrow (sup I)
I is Element of (InclPoset (Ids L)) by YELLOW_2:41;
hence ((IdsMap L) * (SupMap L)) . I = (IdsMap L) . ((SupMap L) . I) by FUNCT_2:15
.= (IdsMap L) . (sup I) by YELLOW_2:def 3
.= downarrow (sup I) by YELLOW_2:def 4 ;
:: thesis: verum

end;

( (IdsMap L) * (SupMap L) is monotone & [(IdsMap L),(SupMap L)] is Galois ) by Th57, YELLOW_2:12;
hence (IdsMap L) * (SupMap L) is closure by Th38; :: thesis: Image ((IdsMap L) * (SupMap L)),L are_isomorphic
take f = (SupMap L) * (inclusion ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic

A2: now :: thesis: for x being Element of (Image ((IdsMap L) * (SupMap L)))
for I being Ideal of L st x = I holds
f . I = sup I

let x be Element of (Image ((IdsMap L) * (SupMap L))); :: thesis: for I being Ideal of L st x = I holds
f . I = sup I
let I be Ideal of L; :: thesis: ( x = I implies f . I = sup I )
assume A3: x = I ; :: thesis: f . I = sup I
hence f . I = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . I) by FUNCT_2:15
.= (SupMap L) . I by A3
.= sup I by YELLOW_2:def 3 ;
:: thesis: verum

end;

A4: f is monotone by YELLOW_2:12;

A5: now :: thesis: for x, y being Element of (Image ((IdsMap L) * (SupMap L))) holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )

let x, y be Element of (Image ((IdsMap L) * (SupMap L))); :: thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
consider Ix being Element of (InclPoset (Ids L)) such that
A6: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10;
thus ( x <= y implies f . x <= f . y ) by A4; :: thesis: ( f . x <= f . y implies x <= y )
assume A7: f . x <= f . y ; :: thesis: x <= y
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58;
then reconsider x9 = x, y9 = y as Ideal of L by YELLOW_2:41;
consider Iy being Element of (InclPoset (Ids L)) such that
A8: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41;
reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A9: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1;
A10: ( f . x9 = sup x9 & f . y9 = sup y9 ) by A2;
( sup (downarrow (sup Ix)) = sup Ix & sup (downarrow (sup Iy)) = sup Iy ) by WAYBEL_0:34;
then downarrow (sup Ix) c= downarrow (sup Iy) by A7, A6, A8, A9, A10, WAYBEL_0:21;
then i1 <= i2 by YELLOW_1:3;
hence x <= y by A6, A8, A9, YELLOW_0:60; :: thesis: verum

end;

A11: rng f = the carrier of L

proof

thus rng f c= the carrier of L ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of L c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in rng f )
assume x in the carrier of L ; :: thesis: x in rng f
then reconsider x = x as Element of L ;
A12: (SupMap L) . (downarrow x) = sup (downarrow x) by YELLOW_2:def 3
.= x by WAYBEL_0:34 ;
A13: downarrow x is Element of (InclPoset (Ids L)) by YELLOW_2:41;
then ((IdsMap L) * (SupMap L)) . (downarrow x) = (IdsMap L) . ((SupMap L) . (downarrow x)) by FUNCT_2:15
.= downarrow x by A12, YELLOW_2:def 4 ;
then downarrow x in rng ((IdsMap L) * (SupMap L)) by A13, FUNCT_2:4;
then A14: downarrow x in the carrier of (Image ((IdsMap L) * (SupMap L))) by YELLOW_0:def 15;
then f . (downarrow x) = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . (downarrow x)) by FUNCT_2:15
.= (SupMap L) . (downarrow x) by A14, FUNCT_1:18 ;
hence x in rng f by A12, A14, FUNCT_2:4; :: thesis: verum

end;

f is one-to-one

proof

let x, y be Element of (Image ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def 1 :: thesis: ( f . x = f . y implies x = y )
assume A15: f . x = f . y ; :: thesis: x = y
consider Ix being Element of (InclPoset (Ids L)) such that
A16: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10;
consider Iy being Element of (InclPoset (Ids L)) such that
A17: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10;
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58;
then reconsider x = x, y = y as Ideal of L by YELLOW_2:41;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41;
A18: sup (downarrow (sup Ix)) = sup Ix by WAYBEL_0:34;
A19: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1;
( f . x = sup x & f . y = sup y ) by A2;
hence x = y by A15, A16, A17, A19, A18, WAYBEL_0:34; :: thesis: verum

end;

hence f is isomorphic by A11, A5, WAYBEL_0:66; :: thesis: verum