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: (IdsMap L) * (SupMap L) is monotone by YELLOW_2:14;
[(IdsMap L),(SupMap L)] is Galois by Th60;
hence (IdsMap L) * (SupMap L) is closure by A1, Th41; :: 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

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:43;
hence ((IdsMap L) * (SupMap L)) . I = (IdsMap L) . ((SupMap L) . I) by FUNCT_2:21
.= (IdsMap L) . (sup I) by YELLOW_2:def 3
.= downarrow (sup I) by YELLOW_2:def 4 ;
:: thesis: verum

end;

A3: now

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 A4: x = I ; :: thesis: f . I = sup I
hence f . I = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . I) by FUNCT_2:21
.= (SupMap L) . I by A4, TMAP_1:91
.= sup I by YELLOW_2:def 3 ;
:: thesis: verum

end;

A5: 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 A6: f . x = f . y ; :: thesis: x = y
consider Ix being Element of (InclPoset (Ids L)) such that
A7: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:12;
consider Iy being Element of (InclPoset (Ids L)) such that
A8: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:12;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:43;
A9: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A2;
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:59;
then reconsider x = x, y = y as Ideal of L by YELLOW_2:43;
A10: ( f . x = sup x & f . y = sup y ) by A3;
( sup (downarrow (sup Ix)) = sup Ix & sup (downarrow (sup Iy)) = sup Iy ) by WAYBEL_0:34;
hence x = y by A6, A7, A8, A9, A10; :: thesis: verum

end;

A11: f is monotone by YELLOW_2:14;
A12: 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 set ; :: 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 ;
A13: (SupMap L) . (downarrow x) = sup (downarrow x) by YELLOW_2:def 3
.= x by WAYBEL_0:34 ;
A14: downarrow x is Element of (InclPoset (Ids L)) by YELLOW_2:43;
then ((IdsMap L) * (SupMap L)) . (downarrow x) = (IdsMap L) . ((SupMap L) . (downarrow x)) by FUNCT_2:21
.= downarrow x by A13, YELLOW_2:def 4 ;
then downarrow x in rng ((IdsMap L) * (SupMap L)) by A14, FUNCT_2:6;
then A15: 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:21
.= (SupMap L) . (downarrow x) by A15, TMAP_1:91 ;
hence x in rng f by A13, A15, FUNCT_2:6; :: thesis: verum

end;

now

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 ) )
thus ( x <= y implies f . x <= f . y ) by A11, Def2; :: thesis: ( f . x <= f . y implies x <= y )
assume A16: f . x <= f . y ; :: thesis: x <= y
consider Ix being Element of (InclPoset (Ids L)) such that
A17: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:12;
consider Iy being Element of (InclPoset (Ids L)) such that
A18: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:12;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:43;
A19: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A2;
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:59;
then reconsider x' = x, y' = y as Ideal of L by YELLOW_2:43;
reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of (InclPoset (Ids L)) by YELLOW_2:43;
A20: ( f . x' = sup x' & f . y' = sup y' ) by A3;
( 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 A16, A17, A18, A19, A20, WAYBEL_0:21;
then i1 <= i2 by YELLOW_1:3;
hence x <= y by A17, A18, A19, YELLOW_0:61; :: thesis: verum

end;

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