let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for x being Element of [:S,T:] holds
( proj1 (wayabove x) c= wayabove (x `1 ) & proj2 (wayabove x) c= wayabove (x `2 ) )
let x be Element of [:S,T:]; :: thesis: ( proj1 (wayabove x) c= wayabove (x `1 ) & proj2 (wayabove x) c= wayabove (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:23;

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

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

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in proj2 (wayabove x) or b in wayabove (x `2 ) )
assume b in proj2 (wayabove x) ; :: thesis: b in wayabove (x `2 )
then consider a being set such that
A4: [a,b] in wayabove x by RELAT_1:def 5;
reconsider b' = b as Element of T by A1, A4, ZFMISC_1:106;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:106;
[a,b'] >> x by A4, WAYBEL_3:8;
then b' >> x `2 by A2, Th18;
hence b in wayabove (x `2 ) ; :: thesis: verum