let S1, S2 be non empty RelStr ; :: thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let D1 be Subset of S1; :: thesis: for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let D2 be Subset of S2; :: thesis: for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let x be Element of S1; :: thesis: for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let y be Element of S2; :: thesis: ( x is_<=_than D1 & y is_<=_than D2 implies [x,y] is_<=_than [:D1,D2:] )
assume that
A1: x is_<=_than D1 and
A2: y is_<=_than D2 ; :: thesis: [x,y] is_<=_than [:D1,D2:]
let b be Element of [:S1,S2:]; :: according to LATTICE3:def 8 :: thesis: ( not b in [:D1,D2:] or [x,y] <= b )
assume b in [:D1,D2:] ; :: thesis: [x,y] <= b
then consider b1, b2 being set such that
A3: ( b1 in D1 & b2 in D2 & b = [b1,b2] ) by ZFMISC_1:def 2;
reconsider b1 = b1 as Element of S1 by A3;
reconsider b2 = b2 as Element of S2 by A3;
( b1 >= x & b2 >= y ) by A1, A2, A3, LATTICE3:def 8;
hence b >= [x,y] by A3, Th11; :: thesis: verum