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