set C = CompactSublatt [:S,T:];
thus [:S,T:] is algebraic ; :: according to WAYBEL_8:def 5 :: thesis: CompactSublatt [:S,T:] is meet-inheriting
let x, y be Element of [:S,T:]; :: according to YELLOW_0:def 16 :: thesis: ( 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:] ; :: thesis: "/\" ({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; :: thesis: verum