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, YELLOW_0:def 16;
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, YELLOW_0:def 16;
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