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 ; :: 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 ;
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 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 z' be Element of ; :: thesis: ( not z' <= x or not z' <= y or z' <= z `1 )
assume ( x >= z' & y >= z' ) ; :: thesis: z' <= z `1
then ( [x,a] >= [z',a] & [y,a] >= [z',a] ) by A3, Th11;
then z >= [z',a] by A5;
hence z' <= z `1 by A6, Th11; :: thesis: verum

end;

consider a being Element of ;
A7: a <= a ;
let x, y be Element of ; :: 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 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 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 z' be Element of ; :: thesis: ( not z' <= x or not z' <= y or z' <= z `2 )
assume ( x >= z' & y >= z' ) ; :: thesis: z' <= z `2
then ( [a,x] >= [a,z'] & [a,y] >= [a,z'] ) by A7, Th11;
then z >= [a,z'] by A9;
hence z' <= z `2 by A10, Th11; :: thesis: verum