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 ; :: 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₂ ) ) )
consider a being Element of ;
A3: a <= a ;
consider z being Element of such that
A4: ( [x,a] <= z & [y,a] <= z ) and
A5: for z' being Element of st [x,a] <= z' & [y,a] <= z' holds
z <= z' by A1, LATTICE3:def 10;
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:23;
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 z' be Element of ; :: thesis: ( not x <= z' or not y <= z' or z `1 <= z' )
assume ( x <= z' & y <= z' ) ; :: thesis: z `1 <= z'
then ( [x,a] <= [z',a] & [y,a] <= [z',a] ) by A3, Th11;
then z <= [z',a] by A5;
hence z `1 <= z' by A6, Th11; :: thesis: verum

end;

consider a being Element of ;
A7: a <= a ;
let x, y be Element of ; :: 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 such that
A8: ( [a,x] <= z & [a,y] <= z ) and
A9: for z' being Element of st [a,x] <= z' & [a,y] <= z' holds
z <= z' by A1, LATTICE3:def 10;
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:23;
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 z' be Element of ; :: thesis: ( not x <= z' or not y <= z' or z `2 <= z' )
assume ( x <= z' & y <= z' ) ; :: thesis: z `2 <= z'
then ( [a,x] <= [a,z'] & [a,y] <= [a,z'] ) by A7, Th11;
then z <= [a,z'] by A9;
hence z `2 <= z' by A10, Th11; :: thesis: verum