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

let x, y be Element of L; :: thesis:
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:

assume x <= y ; :: thesis:
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:

end;

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

assume f . x <= f . y ; :: thesis:
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:

end;

end;

let y be object ; :: thesis:
assume A4: y in the carrier of (CompactSublatt (InclPoset (Ids L))) ; :: thesis:
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:
thus x9 in the carrier of L ; :: thesis:
thus y = f . x9 by A1, A5; :: thesis:

end;

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

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

end;

then f is V13() by WAYBEL_1:def 1;
hence f is isomorphic by A6, A2, WAYBEL_0:66; :: thesis: