let S, T be non empty up-complete Poset; :: thesis: for s being Element of S
for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
let s be Element of S; :: thesis: for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
let t be Element of T; :: thesis: [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: compactbelow [s,t] c= [:(compactbelow s),(compactbelow t):]

let x be object ; :: thesis: ( x in [:(compactbelow s),(compactbelow t):] implies x in compactbelow [s,t] )
assume x in [:(compactbelow s),(compactbelow t):] ; :: thesis: x in compactbelow [s,t]
then consider x1, x2 being object such that
A1: x1 in compactbelow s and
A2: x2 in compactbelow t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
( s >= x1 & t >= x2 ) by A1, A2, WAYBEL_8:4;
then A4: [s,t] >= [x1,x2] by YELLOW_3:11;
A5: ( [x1,x2] `1 = x1 & [x1,x2] `2 = x2 ) ;
( x1 is compact & x2 is compact ) by A1, A2, WAYBEL_8:4;
then [x1,x2] is compact by A5, Th23;
hence x in compactbelow [s,t] by A3, A4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in compactbelow [s,t] or x in [:(compactbelow s),(compactbelow t):] )
assume A6: x in compactbelow [s,t] ; :: thesis: x in [:(compactbelow s),(compactbelow t):]
then reconsider x9 = x as Element of [:S,T:] ;
A7: x9 is compact by A6, WAYBEL_8:4;
then A8: x9 `1 is compact by Th22;
A9: x9 `2 is compact by A7, Th22;
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then A10: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A11: [s,t] >= x9 by A6, WAYBEL_8:4;
then t >= x9 `2 by A10, YELLOW_3:11;
then A12: x `2 in compactbelow t by A9;
s >= x9 `1 by A10, A11, YELLOW_3:11;
then x `1 in compactbelow s by A8;
hence x in [:(compactbelow s),(compactbelow t):] by A10, A12, ZFMISC_1:def 2; :: thesis: verum