for L being non empty RelStr
for S being Subset of L holds
( S is infs-closed iff for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in S )