let L1, L2 be LATTICE; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is arithmetic implies L2 is arithmetic )
assume that
A1: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) and
A2: L1 is arithmetic ; :: thesis: L2 is arithmetic
A3: L1 is algebraic by A2;
then A4: L2 is algebraic by A1, Th17;
A5: CompactSublatt L1 is meet-inheriting by A2, Def5;

now

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) )
reconsider x1 = x2, y1 = y2 as Element of L1 by A1;
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)
A9: L2 is up-complete by A4;
A10: L1 is up-complete by A3;
( x2 is compact & y2 is compact ) by A6, A7, Def1;
then ( x1 is compact & y1 is compact ) by A1, A9, Th9;
then A11: ( x1 in the carrier of (CompactSublatt L1) & y1 in the carrier of (CompactSublatt L1) ) by Def1;
ex_inf_of {x1,y1},L1 by A1, A8, YELLOW_0:14;
then inf {x1,y1} in the carrier of (CompactSublatt L1) by A5, A11, YELLOW_0:def 16;
then A12: inf {x1,y1} is compact by Def1;
inf {x1,y1} = inf {x2,y2} by A1, A8, YELLOW_0:27;
then inf {x2,y2} is compact by A1, A10, A12, Th9;
hence inf {x2,y2} in the carrier of (CompactSublatt L2) by Def1; :: thesis: verum

end;

then CompactSublatt L2 is meet-inheriting by YELLOW_0:def 16;
hence L2 is arithmetic by A4, Def5; :: thesis: verum