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

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 = downarrow y by A1;
then downarrow x = downarrow y by A1;
hence x = y by WAYBEL_0:19; :: 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 (CompactSublatt (InclPoset (Ids L))) implies ex x' being set st
( x' in the carrier of L & y = f . x' ) )
assume A3: y in the carrier of (CompactSublatt (InclPoset (Ids L))) ; :: thesis: ex x' being set st
( x' in the carrier of L & y = f . x' )
the carrier of (CompactSublatt (InclPoset (Ids L))) c= the carrier of (InclPoset (Ids L)) by YELLOW_0:def 13;
then reconsider y' = y as Element of (InclPoset (Ids L)) by A3;
y' is compact by A3, WAYBEL_8:def 1;
then consider x being Element of L such that
A4: y' = downarrow x by Th12;
reconsider x' = x 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'
thus y = f . x' by A1, A4; :: thesis: verum

end;

then A5: rng f = the carrier of (CompactSublatt (InclPoset (Ids L))) by FUNCT_2:16;
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:59;
reconsider fy = f . y as Element of (InclPoset (Ids L)) by YELLOW_0:59;
x <= x ;
then A6: x in downarrow x by WAYBEL_0:17;
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:61; :: thesis: verum

end;

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:60;
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 A6, WAYBEL_0:17; :: thesis: verum

end;

end;

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