for L being non empty antisymmetric complete RelStr
for a being Element of L
for X being set holds
( a = "/\" (X,L) iff ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
a >= b ) ) )