set C = CompactSublatt [:S,T:];
thus
[:S,T:] is algebraic
; WAYBEL_8:def 5 CompactSublatt [:S,T:] is meet-inheriting
let x, y be Element of [:S,T:]; YELLOW_0:def 16 ( not x in the carrier of (CompactSublatt [:S,T:]) or not y in the carrier of (CompactSublatt [:S,T:]) or not ex_inf_of {x,y},[:S,T:] or "/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:]) )
assume that
A1:
x in the carrier of (CompactSublatt [:S,T:])
and
A2:
y in the carrier of (CompactSublatt [:S,T:])
and
ex_inf_of {x,y},[:S,T:]
; "/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:])
A3:
x is compact
by A1, WAYBEL_8:def 1;
then
x `1 is compact
by Th22;
then A4:
x `1 in the carrier of (CompactSublatt S)
by WAYBEL_8:def 1;
A5:
y is compact
by A2, WAYBEL_8:def 1;
then
y `1 is compact
by Th22;
then A6:
y `1 in the carrier of (CompactSublatt S)
by WAYBEL_8:def 1;
x `2 is compact
by A3, Th22;
then A7:
x `2 in the carrier of (CompactSublatt T)
by WAYBEL_8:def 1;
y `2 is compact
by A5, Th22;
then A8:
y `2 in the carrier of (CompactSublatt T)
by WAYBEL_8:def 1;
( CompactSublatt T is meet-inheriting & ex_inf_of {(x `2),(y `2)},T )
by WAYBEL_8:def 5, YELLOW_0:21;
then
inf {(x `2),(y `2)} in the carrier of (CompactSublatt T)
by A7, A8;
then
(x `2) "/\" (y `2) in the carrier of (CompactSublatt T)
by YELLOW_0:40;
then
(x `2) "/\" (y `2) is compact
by WAYBEL_8:def 1;
then A9:
(x "/\" y) `2 is compact
by Th13;
( CompactSublatt S is meet-inheriting & ex_inf_of {(x `1),(y `1)},S )
by WAYBEL_8:def 5, YELLOW_0:21;
then
inf {(x `1),(y `1)} in the carrier of (CompactSublatt S)
by A4, A6;
then
(x `1) "/\" (y `1) in the carrier of (CompactSublatt S)
by YELLOW_0:40;
then
(x `1) "/\" (y `1) is compact
by WAYBEL_8:def 1;
then
(x "/\" y) `1 is compact
by Th13;
then
x "/\" y is compact
by A9, Th23;
then
inf {x,y} is compact
by YELLOW_0:40;
hence
"/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:])
by WAYBEL_8:def 1; verum