let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { f where f is Function of REAL,REAL, a, b, c, d is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) ) } or g in Membership_Funcs REAL )
assume g in { f where f is Function of REAL,REAL, a, b, c, d is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) ) } ; :: thesis: g in Membership_Funcs REAL
then consider f being Function of REAL,REAL, a, b, c, d being Real such that
A1: f = g and
b <> 0 and
A2: for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ;
g is FuzzySet of REAL by A1, A2, MM60;
hence g in Membership_Funcs REAL by Def1; :: thesis: verum