let A be antisymmetric with_infima RelStr ; :: thesis: for a, b, c being Element of A holds
( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds
c >= d ) ) )
let a, b be Element of A; :: thesis: for c being Element of A holds
( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds
c >= d ) ) )
ex x being Element of A st
( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds
x >= c ) ) by LATTICE3:def 11;
hence for c being Element of A holds
( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of A st d <= a & d <= b holds
c >= d ) ) ) by LATTICE3:def 14; :: thesis: verum