let L1, L2 be LATTICE; :: thesis: ( 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 ) ; :: thesis: 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;

L2 is algebraic by A1, A2, WAYBEL13:32;

hence L2 is arithmetic by A16, WAYBEL_8:def 5; :: thesis: verum

assume that

A1: L1,L2 are_isomorphic and

A2: ( L1 is lower-bounded & L1 is arithmetic ) ; :: thesis: 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 :: thesis: 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)

then A16:
CompactSublatt L2 is meet-inheriting
by YELLOW_0:def 16;inf {x2,y2} in the carrier of (CompactSublatt L2)

let x2, y2 be Element of L2; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;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 ; :: thesis: 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; :: thesis: verum

L2 is algebraic by A1, A2, WAYBEL13:32;

hence L2 is arithmetic by A16, WAYBEL_8:def 5; :: thesis: verum