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 consider c, d being set such that
A4: ( c in the carrier of S1 & d in the carrier of S2 & b = [c,d] ) by ZFMISC_1:def 2;
A5: b = [(b `1 ),(b `2 )] by A4, MCART_1:8;
then ( b `1 is_>=_than D1 & b `2 is_>=_than D2 ) by A3, Th29;
then ( x <= b `1 & y <= b `2 ) by A1, A2;
hence [x,y] <= b by A5, Th11; :: thesis: verum