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