theorem :: WAYBEL_2:21

for L being non empty RelStr
for J, x being set
for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )