:: deftheorem Def2 defines FinSups WAYBEL_2:def 2 :
for L being non empty RelStr
for J being set
for f being Function of J, the carrier of L
for b₄ being prenet of L holds
( b₄ = FinSups f iff ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & b₄ = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) );