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 reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1; :: thesis:
A2: g is isomorphic by A1, WAYBEL_0:68;
A3: compactbelow (f . x) c= f .: (compactbelow x)

let z be object ; :: according to TARSKI:def 3 :: thesis:
x in the carrier of L1 ;
then A4: x in dom f by FUNCT_2:def 1;
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
A5: z1 = z and
A6: f . x >= z1 and
A7: z1 is compact ;
A8: g . z1 is compact by A2, A7, Th28;
g . z1 <= g . (f . x) by A2, A6, WAYBEL_0:66;
then g . z1 <= x by A1, A4, FUNCT_1:34;
then A9: g . z1 in compactbelow x by A8, WAYBEL_8:4;
z1 in the carrier of L2 ;
then A10: z1 in rng f by A1, WAYBEL_0:66;
g . z1 in the carrier of L1 ;
then g . z1 in dom f by FUNCT_2:def 1;
then f . (g . z1) in f .: (compactbelow x) by A9, FUNCT_1:def 6;
hence z in f .: (compactbelow x) by A1, A5, A10, FUNCT_1:35; :: thesis:

end;

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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in f .: (compactbelow x) ; :: thesis:
then consider u being object such that
u in dom f and
A11: u in compactbelow x and
A12: z = f . u by FUNCT_1:def 6;
u in { y where y is Element of L1 : ( x >= y & y is compact ) } by A11, WAYBEL_8:def 2;
then consider u1 being Element of L1 such that
A13: u1 = u and
A14: ( x >= u1 & u1 is compact ) ;
( f . u1 <= f . x & f . u1 is compact ) by A1, A14, Th28, WAYBEL_0:66;
hence z in compactbelow (f . x) by A12, A13, WAYBEL_8:4; :: thesis:

end;

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