let L be lower-bounded sup-Semilattice; :: thesis: for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds
f is isomorphic
let f be Function of L,(CompactSublatt (InclPoset (Ids L))); :: thesis: ( ( for x being Element of L holds f . x = downarrow x ) implies f is isomorphic )
assume A1: for x being Element of L holds f . x = downarrow x ; :: thesis: f is isomorphic
A2: for x, y being Element of L holds
( x <= y iff f . x <= f . y )

proof

let x, y be Element of L; :: thesis: ( x <= y iff f . x <= f . y )
reconsider fx = f . x as Element of (InclPoset (Ids L)) by YELLOW_0:58;
reconsider fy = f . y as Element of (InclPoset (Ids L)) by YELLOW_0:58;
thus ( x <= y implies f . x <= f . y ) :: thesis: ( f . x <= f . y implies x <= y )

proof

assume x <= y ; :: thesis: f . x <= f . y
then downarrow x c= downarrow y by WAYBEL_0:21;
then f . x c= downarrow y by A1;
then fx c= fy by A1;
then fx <= fy by YELLOW_1:3;
hence f . x <= f . y by YELLOW_0:60; :: thesis: verum

end;

x <= x ;
then A3: x in downarrow x by WAYBEL_0:17;
thus ( f . x <= f . y implies x <= y ) :: thesis: verum

proof

assume f . x <= f . y ; :: thesis: x <= y
then fx <= fy by YELLOW_0:59;
then fx c= fy by YELLOW_1:3;
then f . x c= downarrow y by A1;
then downarrow x c= downarrow y by A1;
hence x <= y by A3, WAYBEL_0:17; :: thesis: verum

end;

end;

now :: thesis: for y being object st y in the carrier of (CompactSublatt (InclPoset (Ids L))) holds
ex x9 being object st
( x9 in the carrier of L & y = f . x9 )

let y be object ; :: thesis: ( y in the carrier of (CompactSublatt (InclPoset (Ids L))) implies ex x9 being object st
( x9 in the carrier of L & y = f . x9 ) )
assume A4: y in the carrier of (CompactSublatt (InclPoset (Ids L))) ; :: thesis: ex x9 being object st
( x9 in the carrier of L & y = f . x9 )
the carrier of (CompactSublatt (InclPoset (Ids L))) c= the carrier of (InclPoset (Ids L)) by YELLOW_0:def 13;
then reconsider y9 = y as Element of (InclPoset (Ids L)) by A4;
y9 is compact by A4, WAYBEL_8:def 1;
then consider x being Element of L such that
A5: y9 = downarrow x by Th12;
reconsider x9 = x as object ;
take x9 = x9; :: thesis: ( x9 in the carrier of L & y = f . x9 )
thus x9 in the carrier of L ; :: thesis: y = f . x9
thus y = f . x9 by A1, A5; :: thesis: verum

end;

then A6: rng f = the carrier of (CompactSublatt (InclPoset (Ids L))) by FUNCT_2:10;

now :: thesis: for x, y being Element of L st f . x = f . y holds
x = y

let x, y be Element of L; :: thesis: ( f . x = f . y implies x = y )
assume f . x = f . y ; :: thesis: x = y
then f . x = downarrow y by A1;
then downarrow x = downarrow y by A1;
hence x = y by WAYBEL_0:19; :: thesis: verum

end;

then f is one-to-one by WAYBEL_1:def 1;
hence f is isomorphic by A6, A2, WAYBEL_0:66; :: thesis: verum