let S, T be lower-bounded LATTICE; :: thesis: ( [:S,T:] is arithmetic implies ( S is arithmetic & T is arithmetic ) )
assume that
A1: [:S,T:] is algebraic and
A2: CompactSublatt [:S,T:] is meet-inheriting ; :: according to WAYBEL_8:def 5 :: thesis: ( S is arithmetic & T is arithmetic )
[:S,T:] is up-complete by A1;
then A3: ( S is up-complete & T is up-complete ) by WAYBEL_2:11;

hereby :: according to YELLOW_0:def 16,WAYBEL_8:def 5 :: thesis: T is arithmetic

thus S is algebraic by A1, Th69; :: thesis: for x, y being Element of S st x in the carrier of (CompactSublatt S) & y in the carrier of (CompactSublatt S) & ex_inf_of {x,y},S holds
inf {x,y} in the carrier of (CompactSublatt S)
let x, y be Element of S; :: thesis: ( x in the carrier of (CompactSublatt S) & y in the carrier of (CompactSublatt S) & ex_inf_of {x,y},S implies inf {x,y} in the carrier of (CompactSublatt S) )
assume that
A4: ( x in the carrier of (CompactSublatt S) & y in the carrier of (CompactSublatt S) ) and
ex_inf_of {x,y},S ; :: thesis: inf {x,y} in the carrier of (CompactSublatt S)
A5: ex_inf_of {[x,(Bottom T)],[y,(Bottom T)]},[:S,T:] by YELLOW_0:21;
A6: ( [x,(Bottom T)] `1 = x & [y,(Bottom T)] `1 = y & [x,(Bottom T)] `2 = Bottom T & [y,(Bottom T)] `2 = Bottom T ) by MCART_1:7;
( x is compact & y is compact ) by A4, WAYBEL_8:def 1;
then ( [x,(Bottom T)] is compact & [y,(Bottom T)] is compact ) by A3, A6, Th23, WAYBEL_3:15;
then ( [x,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) & [y,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def 1;
then inf {[x,(Bottom T)],[y,(Bottom T)]} in the carrier of (CompactSublatt [:S,T:]) by A2, A5, YELLOW_0:def 16;
then A7: inf {[x,(Bottom T)],[y,(Bottom T)]} is compact by WAYBEL_8:def 1;
(inf {[x,(Bottom T)],[y,(Bottom T)]}) `1 = ([x,(Bottom T)] "/\" [y,(Bottom T)]) `1 by YELLOW_0:40
.= ([x,(Bottom T)] `1 ) "/\" ([y,(Bottom T)] `1 ) by Th13
.= x "/\" ([y,(Bottom T)] `1 ) by MCART_1:7
.= x "/\" y by MCART_1:7 ;
then x "/\" y is compact by A3, A7, Th22;
then inf {x,y} is compact by YELLOW_0:40;
hence inf {x,y} in the carrier of (CompactSublatt S) by WAYBEL_8:def 1; :: thesis: verum

end;

thus T is algebraic by A1, Th69; :: according to WAYBEL_8:def 5 :: thesis: CompactSublatt T is meet-inheriting
let x, y be Element of T; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of (CompactSublatt T) or not y in the carrier of (CompactSublatt T) or not ex_inf_of {x,y},T or "/\" {x,y},T in the carrier of (CompactSublatt T) )
assume that
A8: ( x in the carrier of (CompactSublatt T) & y in the carrier of (CompactSublatt T) ) and
ex_inf_of {x,y},T ; :: thesis: "/\" {x,y},T in the carrier of (CompactSublatt T)
A9: ex_inf_of {[(Bottom S),x],[(Bottom S),y]},[:S,T:] by YELLOW_0:21;
A10: ( [(Bottom S),x] `2 = x & [(Bottom S),y] `2 = y & [(Bottom S),x] `1 = Bottom S & [(Bottom S),y] `1 = Bottom S ) by MCART_1:7;
( x is compact & y is compact ) by A8, WAYBEL_8:def 1;
then ( [(Bottom S),x] is compact & [(Bottom S),y] is compact ) by A3, A10, Th23, WAYBEL_3:15;
then ( [(Bottom S),x] in the carrier of (CompactSublatt [:S,T:]) & [(Bottom S),y] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def 1;
then inf {[(Bottom S),x],[(Bottom S),y]} in the carrier of (CompactSublatt [:S,T:]) by A2, A9, YELLOW_0:def 16;
then A11: inf {[(Bottom S),x],[(Bottom S),y]} is compact by WAYBEL_8:def 1;
(inf {[(Bottom S),x],[(Bottom S),y]}) `2 = ([(Bottom S),x] "/\" [(Bottom S),y]) `2 by YELLOW_0:40
.= ([(Bottom S),x] `2 ) "/\" ([(Bottom S),y] `2 ) by Th13
.= x "/\" ([(Bottom S),y] `2 ) by MCART_1:7
.= x "/\" y by MCART_1:7 ;
then x "/\" y is compact by A3, A11, Th22;
then inf {x,y} is compact by YELLOW_0:40;
hence "/\" {x,y},T in the carrier of (CompactSublatt T) by WAYBEL_8:def 1; :: thesis: verum