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 )
A3: ( S is up-complete & T is up-complete ) by A1, 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) and
A5: y in the carrier of (CompactSublatt S) and
ex_inf_of {x,y},S ; :: thesis: inf {x,y} in the carrier of (CompactSublatt S)
A6: ( [y,(Bottom T)] `1 = y & [y,(Bottom T)] `2 = Bottom T ) ;
y is compact by A5, WAYBEL_8:def 1;
then [y,(Bottom T)] is compact by A3, A6, Th23, WAYBEL_3:15;
then A7: [y,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) by WAYBEL_8:def 1;
A8: ( [x,(Bottom T)] `1 = x & [x,(Bottom T)] `2 = Bottom T ) ;
x is compact by A4, WAYBEL_8:def 1;
then [x,(Bottom T)] is compact by A3, A8, Th23, WAYBEL_3:15;
then ( ex_inf_of {[x,(Bottom T)],[y,(Bottom T)]},[:S,T:] & [x,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def 1, YELLOW_0:21;
then inf {[x,(Bottom T)],[y,(Bottom T)]} in the carrier of (CompactSublatt [:S,T:]) by A2, A7;
then A9: 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)
.= x "/\" y ;
then x "/\" y is compact by A3, A9, 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
A10: x in the carrier of (CompactSublatt T) and
A11: y in the carrier of (CompactSublatt T) and
ex_inf_of {x,y},T ; :: thesis: "/\" ({x,y},T) in the carrier of (CompactSublatt T)
A12: ( [(Bottom S),y] `2 = y & [(Bottom S),y] `1 = Bottom S ) ;
y is compact by A11, WAYBEL_8:def 1;
then [(Bottom S),y] is compact by A3, A12, Th23, WAYBEL_3:15;
then A13: [(Bottom S),y] in the carrier of (CompactSublatt [:S,T:]) by WAYBEL_8:def 1;
A14: ( [(Bottom S),x] `2 = x & [(Bottom S),x] `1 = Bottom S ) ;
x is compact by A10, WAYBEL_8:def 1;
then [(Bottom S),x] is compact by A3, A14, Th23, WAYBEL_3:15;
then ( ex_inf_of {[(Bottom S),x],[(Bottom S),y]},[:S,T:] & [(Bottom S),x] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def 1, YELLOW_0:21;
then inf {[(Bottom S),x],[(Bottom S),y]} in the carrier of (CompactSublatt [:S,T:]) by A2, A13;
then A15: 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)
.= x "/\" y ;
then x "/\" y is compact by A3, A15, 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