let L be non empty complete Poset; ( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )
set i = (IdsMap L) * (SupMap L);
( (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; Image ((IdsMap L) * (SupMap L)),L are_isomorphic
take f = (SupMap L) * (inclusion ((IdsMap L) * (SupMap L))); WAYBEL_1:def 8 f is isomorphic
A4:
f is monotone
by YELLOW_2:12;
A5:
now 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)));
( ( 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;
( f . x <= f . y implies x <= y )assume A7:
f . x <= f . y
;
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;
verum end;
A11:
rng f = the carrier of L
f is V13()
hence
f is isomorphic
by A11, A5, WAYBEL_0:66; verum