let S, T be lower-bounded LATTICE; ( [: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
; WAYBEL_8:def 5 ( S is arithmetic & T is arithmetic )
A3:
( S is up-complete & T is up-complete )
by A1, WAYBEL_2:11;
hereby YELLOW_0:def 16,
WAYBEL_8:def 5 T is arithmetic
thus
S is
algebraic
by A1, Th69;
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;
( 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
;
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;
verum
end;
thus
T is algebraic
by A1, Th69; WAYBEL_8:def 5 CompactSublatt T is meet-inheriting
let x, y be Element of T; YELLOW_0:def 16 ( 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
; "/\" ({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; verum