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;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;

now :: thesis: for x being Element of L2 holds x = sup (compactbelow x)

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

end;

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