let L be non empty RelStr ; :: thesis:
assume A1: ( L is reflexive & L is connected ) ; :: thesis:
thus L is with_infima :: thesis:

proof

let x, y be Element of L; :: according to LATTICE3:def 11 :: thesis:

per cases by A1;

suppose A2: x <= y ; :: thesis:

take z = x; :: thesis:
thus ( z <= x & z <= y ) by A1, A2; :: thesis:
thus for b₁ being Element of the carrier of L holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ; :: thesis:

end;

suppose A3: y <= x ; :: thesis:

take z = y; :: thesis:
thus ( z <= x & z <= y ) by A1, A3; :: thesis:
thus for b₁ being Element of the carrier of L holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ; :: thesis:

end;

end;

end;

let x, y be Element of L; :: according to LATTICE3:def 10 :: thesis:

per cases by A1;

suppose A4: x <= y ; :: thesis:

take z = y; :: thesis:
thus ( z >= x & z >= y ) by A1, A4; :: thesis:
thus for b₁ being Element of the carrier of L holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ; :: thesis:

end;

suppose A5: y <= x ; :: thesis:

take z = x; :: thesis:
thus ( z >= x & z >= y ) by A1, A5; :: thesis:
thus for b₁ being Element of the carrier of L holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ; :: thesis:

end;

end;