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

proof

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

end;

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