for L being antisymmetric with_infima RelStr
for a, b, c being Element of L holds
( c = a "/\" b iff ( c <= a & c <= b & ( for d being Element of L st d <= a & d <= b holds
c >= d ) ) )