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

now

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 A2: f is one-to-one by WAYBEL_1:def 1;

now

let y be set ; :: thesis: ( y in the carrier of (InclPoset (Ids (CompactSublatt L))) implies ex x' being set st
( x' in the carrier of L & y = f . x' ) )
assume y in the carrier of (InclPoset (Ids (CompactSublatt L))) ; :: thesis: ex x' being set st
( x' in the carrier of L & y = f . x' )
then reconsider y' = y as Ideal of (CompactSublatt L) by YELLOW_2:43;
reconsider y1 = y' 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 x' = sup y1 as set ;
take x' = x'; :: thesis: ( x' in the carrier of L & y = f . x' )
thus x' in the carrier of L ; :: thesis: y = f . x'
A3: y' c= compactbelow (sup y1)

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in y' or d in compactbelow (sup y1) )
assume A4: d in y' ; :: thesis: d in compactbelow (sup y1)
then reconsider d1 = d as Element of (CompactSublatt L) ;
reconsider d' = d1 as Element of L by YELLOW_0:59;
A5: d' is compact by WAYBEL_8:def 1;
y' is_<=_than sup y1 by YELLOW_0:32;
then d' <= sup y1 by A4, LATTICE3:def 9;
hence d in compactbelow (sup y1) by A5, WAYBEL_8:4; :: thesis: verum

end;

compactbelow (sup y1) c= y'

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in compactbelow (sup y1) or d in y' )
assume d in compactbelow (sup y1) ; :: thesis: d in y'
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
A6: d1 = d and
A7: d1 <= sup y1 and
A8: d1 is compact ;
d1 << d1 by A8, WAYBEL_3:def 2;
then consider z being Element of L such that
A9: z in y1 and
A10: d1 <= z by A7, WAYBEL_3:def 1;
reconsider d' = d1 as Element of (CompactSublatt L) by A8, WAYBEL_8:def 1;
reconsider z' = z as Element of (CompactSublatt L) by A9;
d' <= z' by A10, YELLOW_0:61;
hence d in y' by A6, A9, WAYBEL_0:def 19; :: thesis: verum

end;

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

end;

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

now

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

A12: ex_sup_of compactbelow x,L by YELLOW_0:17;
A13: ex_sup_of compactbelow y,L by YELLOW_0:17;
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 compactbelow x c= compactbelow y by A1;
then sup (compactbelow x) <= sup (compactbelow y) by A12, A13, 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;

hence f is isomorphic by A2, A11, WAYBEL_0:66; :: thesis: verum