let L1, L2 be LATTICE; ( 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
; L2 is arithmetic
A3:
L2 is algebraic
by A1, A2, Th17;
A4:
CompactSublatt L1 is meet-inheriting
by A2;
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) )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
;
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;
verum end;
then
CompactSublatt L2 is meet-inheriting
by YELLOW_0:def 16;
hence
L2 is arithmetic
by A3; verum