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 8 :: thesis: ( not b in D1 or x <= b )
assume A2: b in D1 ; :: thesis: x <= b
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 8;
hence b >= x by Th11; :: thesis: verum

end;

let a be Element of S2; :: according to LATTICE3:def 8 :: thesis: ( not a in D2 or y <= a )
assume A3: a in D2 ; :: thesis: y <= a
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 8;
hence a >= y by Th11; :: thesis: verum