let a, b be Real; :: thesis: for f being Function of REAL,REAL st ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) holds
f is FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) implies f is FuzzySet of REAL )
assume for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ; :: thesis: f is FuzzySet of REAL
then f in { f where f is Function of REAL,REAL : ex a, b being Real st
for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) } ;
hence f is FuzzySet of REAL by Def1, TrF2; :: thesis: verum