:: deftheorem Def14 defines "/\" LATTICE3:def 14 :
for A being RelStr st A is antisymmetric holds
for a, b being Element of A st 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 ) ) holds
for b₄ being Element of A holds
( b₄ = a "/\" b iff ( b₄ <= a & b₄ <= b & ( for c being Element of A st c <= a & c <= b holds
c <= b₄ ) ) );