let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for x being Element of [:S,T:] holds
( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )
let x be Element of [:S,T:]; :: thesis: ( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;

hereby :: according to TARSKI:def 3 :: thesis: proj2 (compactbelow x) c= compactbelow (x `2)

let a be object ; :: thesis: ( a in proj1 (compactbelow x) implies a in compactbelow (x `1) )
assume a in proj1 (compactbelow x) ; :: thesis: a in compactbelow (x `1)
then consider b being object such that
A3: [a,b] in compactbelow x by XTUPLE_0:def 12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
( [a9,b] `1 = a9 & [a9,b] is compact ) by A3, WAYBEL_8:4;
then A4: a9 is compact by Th22;
[a9,b] <= x by A3, WAYBEL_8:4;
then a9 <= x `1 by A2, YELLOW_3:11;
hence a in compactbelow (x `1) by A4; :: thesis: verum

end;

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in proj2 (compactbelow x) or b in compactbelow (x `2) )
assume b in proj2 (compactbelow x) ; :: thesis: b in compactbelow (x `2)
then consider a being object such that
A5: [a,b] in compactbelow x by XTUPLE_0:def 13;
reconsider a = a as Element of S by A1, A5, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A5, ZFMISC_1:87;
( [a,b9] `2 = b9 & [a,b9] is compact ) by A5, WAYBEL_8:4;
then A6: b9 is compact by Th22;
[a,b9] <= x by A5, WAYBEL_8:4;
then b9 <= x `2 by A2, YELLOW_3:11;
hence b in compactbelow (x `2) by A6; :: thesis: verum