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

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

end;

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