let S, T be antisymmetric with_suprema 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) )
set a = (x "\/" y) `1 ;
set b = (x "\/" y) `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:21;
A3: y = [(y `1),(y `2)] by A1, MCART_1:21;
A4: for d being Element of S st d >= x `1 & d >= y `1 holds
(x "\/" y) `1 <= d

proof

set t = (x `2) "\/" (y `2);
let d be Element of S; :: thesis: ( d >= x `1 & d >= y `1 implies (x "\/" y) `1 <= d )
assume that
A5: d >= x `1 and
A6: d >= y `1 ; :: thesis: (x "\/" y) `1 <= d
(x `2) "\/" (y `2) >= y `2 by YELLOW_0:22;
then A7: [d,((x `2) "\/" (y `2))] >= y by A3, A6, YELLOW_3:11;
(x `2) "\/" (y `2) >= x `2 by YELLOW_0:22;
then [d,((x `2) "\/" (y `2))] >= x by A2, A5, YELLOW_3:11;
then A8: x "\/" y <= [d,((x `2) "\/" (y `2))] by A7, YELLOW_0:22;
[d,((x `2) "\/" (y `2))] `1 = d ;
hence (x "\/" y) `1 <= d by A8, YELLOW_3:12; :: thesis: verum

end;

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

proof

set s = (x `1) "\/" (y `1);
let d be Element of T; :: thesis: ( d >= x `2 & d >= y `2 implies (x "\/" y) `2 <= d )
assume that
A10: d >= x `2 and
A11: d >= y `2 ; :: thesis: (x "\/" y) `2 <= d
(x `1) "\/" (y `1) >= y `1 by YELLOW_0:22;
then A12: [((x `1) "\/" (y `1)),d] >= y by A3, A11, YELLOW_3:11;
(x `1) "\/" (y `1) >= x `1 by YELLOW_0:22;
then [((x `1) "\/" (y `1)),d] >= x by A2, A10, YELLOW_3:11;
then A13: x "\/" y <= [((x `1) "\/" (y `1)),d] by A12, YELLOW_0:22;
[((x `1) "\/" (y `1)),d] `2 = d ;
hence (x "\/" y) `2 <= d by A13, YELLOW_3:12; :: thesis: verum

end;

x "\/" y >= y by YELLOW_0:22;
then A14: ( (x "\/" y) `1 >= y `1 & (x "\/" y) `2 >= y `2 ) by YELLOW_3:12;
x "\/" y >= x by YELLOW_0:22;
then ( (x "\/" y) `1 >= x `1 & (x "\/" y) `2 >= x `2 ) by YELLOW_3:12;
hence ( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) ) by A14, A4, A9, YELLOW_0:18; :: thesis: verum