let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) holds
( ( 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 ) )
let D1 be Subset of S1; :: thesis: for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) holds
( ( 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 ) )
let D2 be Subset of S2; :: thesis: for x being Element of S1
for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) holds
( ( 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 ) )
let x be Element of S1; :: thesis: for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) holds
( ( 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 ) )
let y be Element of S2; :: thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) implies ( ( 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 ) ) )
assume that
A1: ex_sup_of D1,S1 and
A2: ex_sup_of D2,S2 and
A3: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ; :: 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 ) )
thus for c being Element of S1 st c is_>=_than D1 holds
x <= c :: thesis: for d being Element of S2 st d is_>=_than D2 holds
y <= d

proof

A4: sup D2 is_>=_than D2 by A2, YELLOW_0:30;
let b be Element of S1; :: thesis: ( b is_>=_than D1 implies x <= b )
assume b is_>=_than D1 ; :: thesis: x <= b
then [x,y] <= [b,(sup D2)] by A3, A4, Th30;
hence x <= b by Th11; :: thesis: verum

end;

A5: sup D1 is_>=_than D1 by A1, YELLOW_0:30;
let b be Element of S2; :: thesis: ( b is_>=_than D2 implies y <= b )
assume b is_>=_than D2 ; :: thesis: y <= b
then [x,y] <= [(sup D1),b] by A3, A5, Th30;
hence y <= b by Th11; :: thesis: verum