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

A2: now :: thesis:

let x, y be Element of L; :: thesis:
thus ( x <= y implies f . x <= f . y ) :: thesis:

assume x <= y ; :: thesis:
then compactbelow x c= compactbelow y by Th1;
then f . x c= compactbelow y by A1;
then f . x c= f . y by A1;
hence f . x <= f . y by YELLOW_1:3; :: thesis:

end;

thus ( f . x <= f . y implies x <= y ) :: thesis:

assume f . x <= f . y ; :: thesis:
then f . x c= f . y by YELLOW_1:3;
then f . x c= compactbelow y by A1;
then A3: compactbelow x c= compactbelow y by A1;
( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by YELLOW_0:17;
then sup (compactbelow x) <= sup (compactbelow y) by A3, YELLOW_0:34;
then sup (compactbelow x) <= y by WAYBEL_8:def 3;
hence x <= y by WAYBEL_8:def 3; :: thesis:

end;

end;

let y be object ; :: thesis:
assume y in the carrier of (InclPoset (Ids (CompactSublatt L))) ; :: thesis:
then reconsider y9 = y as Ideal of (CompactSublatt L) by YELLOW_2:41;
reconsider y1 = y9 as non empty Subset of L by Th3;
reconsider y1 = y1 as non empty directed Subset of L by YELLOW_2:7;
set x = sup y1;
reconsider x9 = sup y1 as object ;
take x9 = x9; :: thesis:
thus x9 in the carrier of L ; :: thesis:
A4: compactbelow (sup y1) c= y9

let d be object ; :: according to TARSKI:def 3 :: thesis:
assume d in compactbelow (sup y1) ; :: thesis:
then d in { v where v is Element of L : ( sup y1 >= v & v is compact ) } by WAYBEL_8:def 2;
then consider d1 being Element of L such that
A5: d1 = d and
A6: d1 <= sup y1 and
A7: d1 is compact ;
reconsider d9 = d1 as Element of (CompactSublatt L) by A7, WAYBEL_8:def 1;
d1 << d1 by A7, WAYBEL_3:def 2;
then consider z being Element of L such that
A8: z in y1 and
A9: d1 <= z by A6, WAYBEL_3:def 1;
reconsider z9 = z as Element of (CompactSublatt L) by A8;
d9 <= z9 by A9, YELLOW_0:60;
hence d in y9 by A5, A8, WAYBEL_0:def 19; :: thesis:

end;

y9 c= compactbelow (sup y1)

let d be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: d in y9 ; :: thesis:
then reconsider d1 = d as Element of (CompactSublatt L) ;
reconsider d9 = d1 as Element of L by YELLOW_0:58;
y9 is_<=_than sup y1 by YELLOW_0:32;
then ( d9 is compact & d9 <= sup y1 ) by A10, LATTICE3:def 9, WAYBEL_8:def 1;
hence d in compactbelow (sup y1) by WAYBEL_8:4; :: thesis:

end;

hence y = compactbelow (sup y1) by A4, XBOOLE_0:def 10
.= f . x9 by A1 ;
:: thesis:

end;

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

let x, y be Element of L; :: thesis:
assume f . x = f . y ; :: thesis:
then f . x = compactbelow y by A1;
then compactbelow x = compactbelow y by A1;
then sup (compactbelow x) = y by WAYBEL_8:def 3;
hence x = y by WAYBEL_8:def 3; :: thesis:

end;

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