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 8 :: thesis: ( not b in D1 or x <= b )
assume b in D1 ; :: thesis: x <= b
then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87;
then [b, the Element of D2] >= [x,y] by A1;
hence x <= b by Th11; :: thesis: verum

end;

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