let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let D2 be non empty Subset of S2; :: thesis: for x being Element of S1
for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let x be Element of S1; :: thesis: for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let y be Element of S2; :: thesis: ( ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) implies for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b )
assume that
A1: for c being Element of S1 st c is_>=_than D1 holds
x >= c and
A2: for d being Element of S2 st d is_>=_than D2 holds
y >= d ; :: thesis: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let b be Element of [:S1,S2:]; :: thesis: ( b is_>=_than [:D1,D2:] implies [x,y] >= b )
assume A3: b is_>=_than [:D1,D2:] ; :: thesis: [x,y] >= b
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then ex c, d being object st
( c in the carrier of S1 & d in the carrier of S2 & b = [c,d] ) by ZFMISC_1:def 2;
then A4: b = [(b `1),(b `2)] ;
then b `2 is_>=_than D2 by A3, Th29;
then A5: y >= b `2 by A2;
b `1 is_>=_than D1 by A3, A4, Th29;
then x >= b `1 by A1;
hence [x,y] >= b by A4, A5, Th11; :: thesis: verum