:: deftheorem defines fininfs WAYBEL_0:def 28 :
for L being non empty RelStr
for X being Subset of L holds fininfs X = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;