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

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

end;

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