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

consider a being Element of Y;
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₂ ) ) )
consider z being Element of [:X,Y:] such that
A3: ( [x,a] <= z & [y,a] <= z ) and
A4: for z' being Element of [:X,Y:] 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₁ ) ) )
A5: z = [(z `1 ),(z `2 )] by A2, MCART_1:23;
hence ( x <= z `1 & y <= z `1 ) by A3, 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 X; :: thesis: ( not x <= z' or not y <= z' or z `1 <= z' )
assume A6: ( x <= z' & y <= z' ) ; :: thesis: z `1 <= z'
a <= a ;
then ( [x,a] <= [z',a] & [y,a] <= [z',a] ) by A6, Th11;
then z <= [z',a] by A4;
hence z `1 <= z' by A5, Th11; :: thesis: verum

end;

consider a being 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
A7: ( [a,x] <= z & [a,y] <= z ) and
A8: for z' being Element of [:X,Y:] 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₁ ) ) )
A9: z = [(z `1 ),(z `2 )] by A2, MCART_1:23;
hence ( x <= z `2 & y <= z `2 ) by A7, 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 Y; :: thesis: ( not x <= z' or not y <= z' or z `2 <= z' )
assume A10: ( x <= z' & y <= z' ) ; :: thesis: z `2 <= z'
a <= a ;
then ( [a,x] <= [a,z'] & [a,y] <= [a,z'] ) by A10, Th11;
then z <= [a,z'] by A8;
hence z `2 <= z' by A9, Th11; :: thesis: verum