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: L2 is algebraic by A1, A2, Th17;
A4: 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
A5: x2 in the carrier of (CompactSublatt L2) and
A6: y2 in the carrier of (CompactSublatt L2) and
A7: ex_inf_of {x2,y2},L2 ; :: thesis: inf {x2,y2} in the carrier of (CompactSublatt L2)
x2 is compact by A5, Def1;
then x1 is compact by A1, A3, Th9;
then A8: x1 in the carrier of (CompactSublatt L1) by Def1;
y2 is compact by A6, Def1;
then y1 is compact by A1, A3, Th9;
then A9: y1 in the carrier of (CompactSublatt L1) by Def1;
ex_inf_of {x1,y1},L1 by A1, A7, YELLOW_0:14;
then inf {x1,y1} in the carrier of (CompactSublatt L1) by A4, A8, A9, YELLOW_0:def 16;
then A10: inf {x1,y1} is compact by Def1;
inf {x1,y1} = inf {x2,y2} by A1, A7, YELLOW_0:27;
then inf {x2,y2} is compact by A1, A2, A10, 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 A3, Def5; :: thesis: verum