let S1, S2 be non empty RelStr ; 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; 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; 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; 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; ( 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 )
; [x,y] is_>=_than [:D1,D2:]
let b be Element of [:S1,S2:]; LATTICE3:def 9 ( not b in [:D1,D2:] or b <= [x,y] )
assume
b in [:D1,D2:]
; b <= [x,y]
then consider b1, b2 being object 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 S2 by A3;
reconsider b1 = b1 as Element of S1 by A2;
( b1 <= x & b2 <= y )
by A1, A2, A3;
hence
b <= [x,y]
by A4, Th11; verum