let L be non empty RelStr ; :: thesis: 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 )
let J, x be set ; :: thesis: for f being Function of J, the carrier of L holds
( x is Element of (FinSups f) iff x is Element of Fin J )
let f be Function of J, the carrier of L; :: thesis: ( x is Element of (FinSups f) iff x is Element of Fin J )
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) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
hence ( x is Element of (FinSups f) iff x is Element of Fin J ) ; :: thesis: verum