let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis:
let x be Element of [:S,T:]; :: thesis:
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:23;

hereby :: according to TARSKI:def 3 :: thesis:

let a be set ; :: thesis:
assume a in proj1 (compactbelow x) ; :: thesis:
then consider b being set such that
A3: [a,b] in compactbelow x by RELAT_1:def 4;
reconsider a' = a as Element of S by A1, A3, ZFMISC_1:106;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:106;
A4: ( [a',b] `1 = a' & [a',b] `2 = b ) by MCART_1:7;
( [a',b] <= x & [a',b] is compact ) by A3, WAYBEL_8:4;
then ( a' <= x `1 & a' is compact ) by A2, A4, Th22, YELLOW_3:11;
hence a in compactbelow (x `1 ) ; :: thesis:

end;

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in proj2 (compactbelow x) ; :: thesis:
then consider a being set such that
A5: [a,b] in compactbelow x by RELAT_1:def 5;
reconsider b' = b as Element of T by A1, A5, ZFMISC_1:106;
reconsider a = a as Element of S by A1, A5, ZFMISC_1:106;
A6: ( [a,b'] `1 = a & [a,b'] `2 = b' ) by MCART_1:7;
( [a,b'] <= x & [a,b'] is compact ) by A5, WAYBEL_8:4;
then ( b' <= x `2 & b' is compact ) by A2, A6, Th22, YELLOW_3:11;
hence b in compactbelow (x `2 ) ; :: thesis: