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