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

proof

set a = the Element of D2;
let b be Element of S1; :: according to LATTICE3:def 9 :: thesis: ( not b in D1 or b <= x )
assume b in D1 ; :: thesis: b <= x
then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87;
then [b, the Element of D2] <= [x,y] by A1;
hence b <= x by Th11; :: thesis: verum

end;

set b = the Element of D1;
let a be Element of S2; :: according to LATTICE3:def 9 :: thesis: ( not a in D2 or a <= y )
assume a in D2 ; :: thesis: a <= y
then [ the Element of D1,a] in [:D1,D2:] by ZFMISC_1:87;
then [ the Element of D1,a] <= [x,y] by A1;
hence a <= y by Th11; :: thesis: verum