let X, Y be non empty reflexive RelStr ; :: thesis: ( [:X,Y:] is with_suprema implies ( X is with_suprema & Y is with_suprema ) )
assume A1: [:X,Y:] is with_suprema ; :: thesis: ( X is with_suprema & Y is with_suprema )
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
thus X is with_suprema :: thesis: Y is with_suprema

proof

let x, y be Element of X; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of X st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of X holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
set a = the Element of Y;
A3: the Element of Y <= the Element of Y ;
consider z being Element of [:X,Y:] such that
A4: ( [x, the Element of Y] <= z & [y, the Element of Y] <= z ) and
A5: for z9 being Element of [:X,Y:] st [x, the Element of Y] <= z9 & [y, the Element of Y] <= z9 holds
z <= z9 by A1;
take z `1 ; :: thesis: ( x <= z `1 & y <= z `1 & ( for b<sub>1</sub> being Element of the carrier of X holds
( not x <= b<sub>1</sub> or not y <= b<sub>1</sub> or z `1 <= b₁ ) ) )
A6: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x <= z `1 & y <= z `1 ) by A4, Th11; :: thesis: for b₁ being Element of the carrier of X holds
( not x <= b₁ or not y <= b₁ or z `1 <= b<sub>1</sub> )
let z9 be Element of X; :: thesis: ( not x <= z9 or not y <= z9 or z `1 <= z9 )
assume ( x <= z9 & y <= z9 ) ; :: thesis: z `1 <= z9
then ( [x, the Element of Y] <= [z9, the Element of Y] & [y, the Element of Y] <= [z9, the Element of Y] ) by A3, Th11;
then z <= [z9, the Element of Y] by A5;
hence z `1 <= z9 by A6, Th11; :: thesis: verum

end;

set a = the Element of X;
A7: the Element of X <= the Element of X ;
let x, y be Element of Y; :: according to LATTICE3:def 10 :: thesis: ex b₁ being Element of the carrier of Y st
( x <= b₁ & y <= b₁ & ( for b₂ being Element of the carrier of Y holds
( not x <= b₂ or not y <= b₂ or b₁ <= b₂ ) ) )
consider z being Element of [:X,Y:] such that
A8: ( [ the Element of X,x] <= z & [ the Element of X,y] <= z ) and
A9: for z9 being Element of [:X,Y:] st [ the Element of X,x] <= z9 & [ the Element of X,y] <= z9 holds
z <= z9 by A1;
take z `2 ; :: thesis: ( x <= z `2 & y <= z `2 & ( for b<sub>1</sub> being Element of the carrier of Y holds
( not x <= b<sub>1</sub> or not y <= b<sub>1</sub> or z `2 <= b₁ ) ) )
A10: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x <= z `2 & y <= z `2 ) by A8, Th11; :: thesis: for b₁ being Element of the carrier of Y holds
( not x <= b₁ or not y <= b₁ or z `2 <= b<sub>1</sub> )
let z9 be Element of Y; :: thesis: ( not x <= z9 or not y <= z9 or z `2 <= z9 )
assume ( x <= z9 & y <= z9 ) ; :: thesis: z `2 <= z9
then ( [ the Element of X,x] <= [ the Element of X,z9] & [ the Element of X,y] <= [ the Element of X,z9] ) by A7, Th11;
then z <= [ the Element of X,z9] by A9;
hence z `2 <= z9 by A10, Th11; :: thesis: verum