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

A2: now :: thesis: for x, y being Element of L holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )

let x, y be Element of L; :: thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
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 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: verum

end;

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

proof

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

end;

end;

now :: thesis: for y being object st y in the carrier of (InclPoset (Ids (CompactSublatt 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 (InclPoset (Ids (CompactSublatt L))) implies ex x9 being object st
( x9 in the carrier of L & y = f . x9 ) )
assume y in the carrier of (InclPoset (Ids (CompactSublatt L))) ; :: thesis: ex x9 being object st
( x9 in the carrier of L & y = f . x9 )
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: ( x9 in the carrier of L & y = f . x9 )
thus x9 in the carrier of L ; :: thesis: y = f . x9
A4: compactbelow (sup y1) c= y9

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in compactbelow (sup y1) or d in y9 )
assume d in compactbelow (sup y1) ; :: thesis: d in y9
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: verum

end;

y9 c= compactbelow (sup y1)

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in y9 or d in compactbelow (sup y1) )
assume A10: d in y9 ; :: thesis: d in compactbelow (sup y1)
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: verum

end;

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

end;

then A11: rng f = the carrier of (InclPoset (Ids (CompactSublatt 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 = 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: verum

end;

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