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:21;

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

let a be object ; :: thesis:
assume a in proj1 (waybelow x) ; :: thesis:
then consider b being object such that
A3: [a,b] in waybelow 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] << x by A3, WAYBEL_3:7;
then a9 << x `1 by A2, Th18;
hence a in waybelow (x `1) ; :: thesis:

end;

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in proj2 (waybelow x) ; :: thesis:
then consider a being object such that
A4: [a,b] in waybelow x by XTUPLE_0:def 13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
[a,b9] << x by A4, WAYBEL_3:7;
then b9 << x `2 by A2, Th18;
hence b in waybelow (x `2) ; :: thesis: