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₁ ) ) )
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: ( 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:21;
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, 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 z9 <= z `1 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 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: ( [ 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: ( 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:21;
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 ( [ 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 z9 <= z `2 by A10, Th11; :: thesis: verum