thus [:S,T:] is algebraic ; :: according to WAYBEL_8:def 5 :: thesis: CompactSublatt [:S,T:] is meet-inheriting
set C = CompactSublatt [:S,T:];
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 A1: ( x in the carrier of (CompactSublatt [:S,T:]) & y in the carrier of (CompactSublatt [:S,T:]) & ex_inf_of {x,y},[:S,T:] ) ; :: thesis: "/\" {x,y},[:S,T:] in the carrier of (CompactSublatt [:S,T:])
A2: ( CompactSublatt S is meet-inheriting & CompactSublatt T is meet-inheriting ) by WAYBEL_8:def 5;
A3: ( ex_inf_of {(x `1 ),(y `1 )},S & ex_inf_of {(x `2 ),(y `2 )},T ) by YELLOW_0:21;
( x is compact & y is compact ) by A1, WAYBEL_8:def 1;
then ( x `1 is compact & y `1 is compact & x `2 is compact & y `2 is compact ) by Th22;
then ( x `1 in the carrier of (CompactSublatt S) & y `1 in the carrier of (CompactSublatt S) & x `2 in the carrier of (CompactSublatt T) & y `2 in the carrier of (CompactSublatt T) ) by WAYBEL_8:def 1;
then ( inf {(x `1 ),(y `1 )} in the carrier of (CompactSublatt S) & inf {(x `2 ),(y `2 )} in the carrier of (CompactSublatt T) ) by A2, A3, YELLOW_0:def 16;
then ( (x `1 ) "/\" (y `1 ) in the carrier of (CompactSublatt S) & (x `2 ) "/\" (y `2 ) in the carrier of (CompactSublatt T) ) by YELLOW_0:40;
then ( (x `1 ) "/\" (y `1 ) is compact & (x `2 ) "/\" (y `2 ) is compact ) by WAYBEL_8:def 1;
then ( (x "/\" y) `1 is compact & (x "/\" y) `2 is compact ) by Th13;
then x "/\" y is compact by 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