let S1, S2 be non empty antisymmetric RelStr ; 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; 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; 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; 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; ( ( 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
; for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b
let b be Element of [:S1,S2:]; ( b is_>=_than [:D1,D2:] implies [x,y] <= b )
assume A3:
b is_>=_than [:D1,D2:]
; [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; verum