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 ;
A4: g is isomorphic by ;
A5: L2 is up-complete LATTICE by ;
now :: thesis: for x2, y2 being Element of L2 st x2 in the carrier of () & y2 in the carrier of () & ex_inf_of {x2,y2},L2 holds
inf {x2,y2} in the carrier of ()
let x2, y2 be Element of L2; :: thesis: ( x2 in the carrier of () & y2 in the carrier of () & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of () )
assume that
A6: x2 in the carrier of () and
A7: y2 in the carrier of () and
A8: ex_inf_of {x2,y2},L2 ; :: thesis: inf {x2,y2} in the carrier of ()
x2 is compact by ;
then g . x2 is compact by ;
then A9: g . x2 in the carrier of () by WAYBEL_8:def 1;
y2 is compact by ;
then g . y2 is compact by ;
then A10: g . y2 in the carrier of () 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 ;
y2 in the carrier of L2 ;
then A13: y2 in dom g by FUNCT_2:def 1;
g is infs-preserving by ;
then A14: g preserves_inf_of {x2,y2} by WAYBEL_0:def 32;
then ex_inf_of g .: {x2,y2},L1 by ;
then ex_inf_of {(g . x2),(g . y2)},L1 by ;
then inf {(g . x2),(g . y2)} in the carrier of () by ;
then A15: inf {(g . x2),(g . y2)} is compact by WAYBEL_8:def 1;
g . (inf {x2,y2}) = inf (g .: {x2,y2}) by
.= inf {(g . x2),(g . y2)} by ;
then inf {x2,y2} is compact by ;
hence inf {x2,y2} in the carrier of () by WAYBEL_8:def 1; :: thesis: verum
end;
then A16: CompactSublatt L2 is meet-inheriting by YELLOW_0:def 16;
L2 is algebraic by ;
hence L2 is arithmetic by ; :: thesis: verum