let S, T be non empty RelStr ; :: thesis: for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let s be Element of S; :: thesis: for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let t be Element of T; :: thesis: [:(downarrow s),(downarrow t):] = downarrow [s,t]
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;

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

let x be set ; :: thesis: ( x in [:(downarrow s),(downarrow t):] implies x in downarrow [s,t] )
assume x in [:(downarrow s),(downarrow t):] ; :: thesis: x in downarrow [s,t]
then consider x1, x2 being set such that
A2: ( x1 in downarrow s & x2 in downarrow t & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of S by A2;
reconsider x2 = x2 as Element of T by A2;
( s >= x1 & t >= x2 ) by A2, WAYBEL_0:17;
then [s,t] >= [x1,x2] by YELLOW_3:11;
hence x in downarrow [s,t] by A2, WAYBEL_0:17; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow [s,t] or x in [:(downarrow s),(downarrow t):] )
assume A3: x in downarrow [s,t] ; :: thesis: x in [:(downarrow s),(downarrow t):]
then reconsider x' = x as Element of [:S,T:] ;
A4: x' = [(x' `1 ),(x' `2 )] by A1, MCART_1:23;
[s,t] >= x' by A3, WAYBEL_0:17;
then ( s >= x' `1 & t >= x' `2 ) by A4, YELLOW_3:11;
then ( x `1 in downarrow s & x `2 in downarrow t ) by WAYBEL_0:17;
hence x in [:(downarrow s),(downarrow t):] by A4, MCART_1:11; :: thesis: verum