let L1, L2 be non empty Poset; ( 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 )
; 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 for x being Element of L2 holds x = sup (compactbelow x)let x be
Element of
L2;
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
;
verum end;
hence
L2 is satisfying_axiom_K
by WAYBEL_8:def 3; verum