let S, T be antisymmetric with_infima RelStr ; :: thesis: for x, y being Element of [:S,T:] holds
( (x "/\" y) `1 = (x `1 ) "/\" (y `1 ) & (x "/\" y) `2 = (x `2 ) "/\" (y `2 ) )
let x, y be Element of [:S,T:]; :: thesis: ( (x "/\" y) `1 = (x `1 ) "/\" (y `1 ) & (x "/\" y) `2 = (x `2 ) "/\" (y `2 ) )
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then A1: ( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] ) by MCART_1:23;
set a = (x "/\" y) `1 ;
set b = (x "/\" y) `2 ;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
then A2: ( (x "/\" y) `1 <= x `1 & (x "/\" y) `1 <= y `1 & (x "/\" y) `2 <= x `2 & (x "/\" y) `2 <= y `2 ) by YELLOW_3:12;
A3: for d being Element of S st d <= x `1 & d <= y `1 holds
(x "/\" y) `1 >= d

proof

let d be Element of S; :: thesis: ( d <= x `1 & d <= y `1 implies (x "/\" y) `1 >= d )
assume A4: ( d <= x `1 & d <= y `1 ) ; :: thesis: (x "/\" y) `1 >= d
set t = (x `2 ) "/\" (y `2 );
( (x `2 ) "/\" (y `2 ) <= x `2 & (x `2 ) "/\" (y `2 ) <= y `2 ) by YELLOW_0:23;
then ( [d,((x `2 ) "/\" (y `2 ))] <= x & [d,((x `2 ) "/\" (y `2 ))] <= y ) by A1, A4, YELLOW_3:11;
then A5: x "/\" y >= [d,((x `2 ) "/\" (y `2 ))] by YELLOW_0:23;
[d,((x `2 ) "/\" (y `2 ))] `1 = d by MCART_1:7;
hence (x "/\" y) `1 >= d by A5, YELLOW_3:12; :: thesis: verum

end;

for d being Element of T st d <= x `2 & d <= y `2 holds
(x "/\" y) `2 >= d

proof

let d be Element of T; :: thesis: ( d <= x `2 & d <= y `2 implies (x "/\" y) `2 >= d )
assume A6: ( d <= x `2 & d <= y `2 ) ; :: thesis: (x "/\" y) `2 >= d
set s = (x `1 ) "/\" (y `1 );
( (x `1 ) "/\" (y `1 ) <= x `1 & (x `1 ) "/\" (y `1 ) <= y `1 ) by YELLOW_0:23;
then ( [((x `1 ) "/\" (y `1 )),d] <= x & [((x `1 ) "/\" (y `1 )),d] <= y ) by A1, A6, YELLOW_3:11;
then A7: x "/\" y >= [((x `1 ) "/\" (y `1 )),d] by YELLOW_0:23;
[((x `1 ) "/\" (y `1 )),d] `2 = d by MCART_1:7;
hence (x "/\" y) `2 >= d by A7, YELLOW_3:12; :: thesis: verum

end;

hence ( (x "/\" y) `1 = (x `1 ) "/\" (y `1 ) & (x "/\" y) `2 = (x `2 ) "/\" (y `2 ) ) by A2, A3, YELLOW_0:19; :: thesis: verum