let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { f where f is Function of REAL,REAL, a, b, c is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) ) } or g in Membership_Funcs REAL )

assume g in { f where f is Function of REAL,REAL, a, b, c is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) ) } ; :: thesis: g in Membership_Funcs REAL

then consider f being Function of REAL,REAL, a, b, c being Real such that

A1: f = g and

A0: b <> 0 and

A2: for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ;

g is FuzzySet of REAL by A0, A1, A2, GauF07;

hence g in Membership_Funcs REAL by Def1; :: thesis: verum

assume g in { f where f is Function of REAL,REAL, a, b, c is Real : ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) ) } ; :: thesis: g in Membership_Funcs REAL

then consider f being Function of REAL,REAL, a, b, c being Real such that

A1: f = g and

A0: b <> 0 and

A2: for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ;

g is FuzzySet of REAL by A0, A1, A2, GauF07;

hence g in Membership_Funcs REAL by Def1; :: thesis: verum