let L1, L2 be LATTICE; ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is arithmetic implies L2 is arithmetic )
assume that
A1:
L1,L2 are_isomorphic
and
A2:
( L1 is lower-bounded & L1 is arithmetic )
; L2 is arithmetic
consider f being Function of L1,L2 such that
A3:
f is isomorphic
by A1;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A4:
g is isomorphic
by A3, WAYBEL_0:68;
A5:
L2 is up-complete LATTICE
by A1, A2, WAYBEL13:30;
now for x2, y2 being Element of L2 st x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 holds
inf {x2,y2} in the carrier of (CompactSublatt L2)let x2,
y2 be
Element of
L2;
( x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of (CompactSublatt L2) )assume that A6:
x2 in the
carrier of
(CompactSublatt L2)
and A7:
y2 in the
carrier of
(CompactSublatt L2)
and A8:
ex_inf_of {x2,y2},
L2
;
inf {x2,y2} in the carrier of (CompactSublatt L2)
x2 is
compact
by A6, WAYBEL_8:def 1;
then
g . x2 is
compact
by A2, A4, A5, WAYBEL13:28;
then A9:
g . x2 in the
carrier of
(CompactSublatt L1)
by WAYBEL_8:def 1;
y2 is
compact
by A7, WAYBEL_8:def 1;
then
g . y2 is
compact
by A2, A4, A5, WAYBEL13:28;
then A10:
g . y2 in the
carrier of
(CompactSublatt L1)
by WAYBEL_8:def 1;
x2 in the
carrier of
L2
;
then A11:
x2 in dom g
by FUNCT_2:def 1;
A12:
CompactSublatt L1 is
meet-inheriting
by A2, WAYBEL_8:def 5;
y2 in the
carrier of
L2
;
then A13:
y2 in dom g
by FUNCT_2:def 1;
g is
infs-preserving
by A4, WAYBEL13:20;
then A14:
g preserves_inf_of {x2,y2}
by WAYBEL_0:def 32;
then
ex_inf_of g .: {x2,y2},
L1
by A8, WAYBEL_0:def 30;
then
ex_inf_of {(g . x2),(g . y2)},
L1
by A11, A13, FUNCT_1:60;
then
inf {(g . x2),(g . y2)} in the
carrier of
(CompactSublatt L1)
by A9, A10, A12, YELLOW_0:def 16;
then A15:
inf {(g . x2),(g . y2)} is
compact
by WAYBEL_8:def 1;
g . (inf {x2,y2}) =
inf (g .: {x2,y2})
by A8, A14, WAYBEL_0:def 30
.=
inf {(g . x2),(g . y2)}
by A11, A13, FUNCT_1:60
;
then
inf {x2,y2} is
compact
by A2, A4, A5, A15, WAYBEL13:28;
hence
inf {x2,y2} in the
carrier of
(CompactSublatt L2)
by WAYBEL_8:def 1;
verum end;
then A16:
CompactSublatt L2 is meet-inheriting
by YELLOW_0:def 16;
L2 is algebraic
by A1, A2, WAYBEL13:32;
hence
L2 is arithmetic
by A16, WAYBEL_8:def 5; verum