let S, T be antisymmetric with_infima RelStr ; 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:]; ( (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:23;
A3:
y = [(y `1 ),(y `2 )]
by A1, MCART_1:23;
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;
( d <= x `1 & d <= y `1 implies (x "/\" y) `1 >= d )
assume that A5:
d <= x `1
and A6:
d <= y `1
;
(x "/\" y) `1 >= d
(x `2 ) "/\" (y `2 ) <= y `2
by YELLOW_0:23;
then A7:
[d,((x `2 ) "/\" (y `2 ))] <= y
by A3, A6, YELLOW_3:11;
(x `2 ) "/\" (y `2 ) <= x `2
by YELLOW_0:23;
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:23;
[d,((x `2 ) "/\" (y `2 ))] `1 = d
by MCART_1:7;
hence
(x "/\" y) `1 >= d
by A8, YELLOW_3:12;
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;
( d <= x `2 & d <= y `2 implies (x "/\" y) `2 >= d )
assume that A10:
d <= x `2
and A11:
d <= y `2
;
(x "/\" y) `2 >= d
(x `1 ) "/\" (y `1 ) <= y `1
by YELLOW_0:23;
then A12:
[((x `1 ) "/\" (y `1 )),d] <= y
by A3, A11, YELLOW_3:11;
(x `1 ) "/\" (y `1 ) <= x `1
by YELLOW_0:23;
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:23;
[((x `1 ) "/\" (y `1 )),d] `2 = d
by MCART_1:7;
hence
(x "/\" y) `2 >= d
by A13, YELLOW_3:12;
verum
end;
x "/\" y <= y
by YELLOW_0:23;
then A14:
( (x "/\" y) `1 <= y `1 & (x "/\" y) `2 <= y `2 )
by YELLOW_3:12;
x "/\" y <= x
by YELLOW_0:23;
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:19; verum