let L1, L2 be non empty Poset; :: thesis: ( L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K implies L2 is satisfying_axiom_K )
assume that
A1: L1,L2 are_isomorphic and
A2: ( L1 is complete & L1 is satisfying_axiom_K ) ; :: thesis: L2 is satisfying_axiom_K
consider f being Function of L1,L2 such that
A3: f is isomorphic by A1, WAYBEL_1:def 8;
A4: f is one-to-one by A3;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;

now

let x be Element of L2; :: thesis: x = sup (compactbelow x)
f is sups-preserving by A3;
then A5: f preserves_sup_of compactbelow (g . x) by WAYBEL_0:def 33;
A6: ex_sup_of compactbelow (g . x),L1 by A2, YELLOW_0:17;
A7: L1 is non empty complete Poset by A2;
then A8: L2 is non empty up-complete Poset by A1, Th30;
( not the carrier of L1 is empty & x in the carrier of L2 ) ;
then x in dom g by FUNCT_2:def 1;
then A9: x in rng f by A4, FUNCT_1:55;
hence x = f . (g . x) by A4, FUNCT_1:57
.= f . (sup (compactbelow (g . x))) by A2, WAYBEL_8:def 3
.= sup (f .: (compactbelow (g . x))) by A5, A6, WAYBEL_0:def 31
.= sup (compactbelow (f . (g . x))) by A3, A7, A8, Th29
.= sup (compactbelow x) by A4, A9, FUNCT_1:57 ;
:: thesis: verum

end;

hence L2 is satisfying_axiom_K by WAYBEL_8:def 3; :: thesis: verum