let S1, S2 be non empty RelStr ; :: thesis: for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let D be Subset of [:S1,S2:]; :: thesis: for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let x be Element of S1; :: thesis: for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let y be Element of S2; :: thesis: ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
set D1 = proj1 D;
set D2 = proj2 D;

hereby :: thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D implies [x,y] is_>=_than D )

assume A1: [x,y] is_>=_than D ; :: thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D )
thus x is_>=_than proj1 D :: thesis: y is_>=_than proj2 D

proof

let q be Element of S1; :: according to LATTICE3:def 9 :: thesis: ( not q in proj1 D or q <= x )
assume q in proj1 D ; :: thesis: q <= x
then consider z being object such that
A2: [q,z] in D by XTUPLE_0:def 12;
reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def 13;
reconsider z = z as Element of d2 by A2, XTUPLE_0:def 13;
[x,y] >= [q,z] by A1, A2;
hence q <= x by Th11; :: thesis: verum

end;

thus y is_>=_than proj2 D :: thesis: verum

proof

let q be Element of S2; :: according to LATTICE3:def 9 :: thesis: ( not q in proj2 D or q <= y )
assume q in proj2 D ; :: thesis: q <= y
then consider z being object such that
A3: [z,q] in D by XTUPLE_0:def 13;
reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def 12;
reconsider z = z as Element of d1 by A3, XTUPLE_0:def 12;
[x,y] >= [z,q] by A1, A3;
hence q <= y by Th11; :: thesis: verum

end;

end;

assume ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ; :: thesis: [x,y] is_>=_than D
then A4: [x,y] is_>=_than [:(proj1 D),(proj2 D):] by Th30;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then D c= [:(proj1 D),(proj2 D):] by Th1;
hence [x,y] is_>=_than D by A4; :: thesis: verum