let L1, L2 be non empty up-complete Poset; :: thesis:
let f be Function of L1,L2; :: thesis:
assume A1: f is isomorphic ; :: thesis:
then A2: f is one-to-one ;
reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67;
A3: g is isomorphic by A1, WAYBEL_0:68;
let x be Element of L1; :: thesis:
A4: f .: (compactbelow x) c= compactbelow (f . x)

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in f .: (compactbelow x) ; :: thesis:
then consider u being set such that
u in dom f and
A5: u in compactbelow x and
A6: z = f . u by FUNCT_1:def 12;
u in { y where y is Element of L1 : ( x >= y & y is compact ) } by A5, WAYBEL_8:def 2;
then consider u1 being Element of L1 such that
A7: u1 = u and
A8: x >= u1 and
A9: u1 is compact ;
A10: f . u1 <= f . x by A1, A8, WAYBEL_0:66;
f . u1 is compact by A1, A9, Th28;
hence z in compactbelow (f . x) by A6, A7, A10, WAYBEL_8:4; :: thesis:

end;

compactbelow (f . x) c= f .: (compactbelow x)

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in compactbelow (f . x) ; :: thesis:
then z in { y where y is Element of L2 : ( f . x >= y & y is compact ) } by WAYBEL_8:def 2;
then consider z1 being Element of L2 such that
A11: z1 = z and
A12: f . x >= z1 and
A13: z1 is compact ;
( g . z1 in the carrier of L1 & x in the carrier of L1 & not the carrier of L2 is empty ) ;
then A14: ( g . z1 in dom f & x in dom f ) by FUNCT_2:def 1;
z1 in the carrier of L2 ;
then A15: z1 in rng f by A1, WAYBEL_0:66;
g . z1 <= g . (f . x) by A3, A12, WAYBEL_0:66;
then A16: g . z1 <= x by A2, A14, FUNCT_1:56;
g . z1 is compact by A3, A13, Th28;
then g . z1 in compactbelow x by A16, WAYBEL_8:4;
then f . (g . z1) in f .: (compactbelow x) by A14, FUNCT_1:def 12;
hence z in f .: (compactbelow x) by A2, A11, A15, FUNCT_1:57; :: thesis:

end;

hence f .: (compactbelow x) = compactbelow (f . x) by A4, XBOOLE_0:def 10; :: thesis: