let L be antisymmetric RelStr ; :: thesis: ( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L )

hereby :: thesis: ( ( for a, b being Element of L holds ex_inf_of {a,b},L ) implies L is with_infima )

assume A1: L is with_infima ; :: thesis: for a, b being Element of L holds ex_inf_of {a,b},L
let a, b be Element of L; :: thesis: ex_inf_of {a,b},L
ex z being Element of L st
( a >= z & b >= z & ( for z9 being Element of L st a >= z9 & b >= z9 holds
z >= z9 ) ) by A1;
hence ex_inf_of {a,b},L by Th19; :: thesis: verum

end;

assume A2: for a, b being Element of L holds ex_inf_of {a,b},L ; :: thesis: L is with_infima
let x, y be Element of L; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of L st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of L holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
take x "/\" y ; :: thesis: ( x "/\" y <= x & x "/\" y <= y & ( for b₁ being Element of the carrier of L holds
( not b₁ <= x or not b₁ <= y or b₁ <= x "/\" y ) ) )
ex_inf_of {x,y},L by A2;
hence ( x "/\" y <= x & x "/\" y <= y & ( for b₁ being Element of the carrier of L holds
( not b₁ <= x or not b₁ <= y or b₁ <= x "/\" y ) ) ) by Th19; :: thesis: verum