A1:
Membership_Funcs REAL c= { f where f is Function of REAL,REAL : f is FuzzySet of REAL }

proof

{ f where f is Function of REAL,REAL : f is FuzzySet of REAL } c= Membership_Funcs REAL
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in Membership_Funcs REAL or f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } )

assume f in Membership_Funcs REAL ; :: thesis: f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL }

then ex f0 being Membership_Func of REAL st

( f0 = f & dom f0 = REAL ) by LM1;

hence f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } ; :: thesis: verum

end;assume f in Membership_Funcs REAL ; :: thesis: f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL }

then ex f0 being Membership_Func of REAL st

( f0 = f & dom f0 = REAL ) by LM1;

hence f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } ; :: thesis: verum

proof

hence
Membership_Funcs REAL = { f where f is Function of REAL,REAL : f is FuzzySet of REAL }
by XBOOLE_0:def 10, A1; :: thesis: verum
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } or f in Membership_Funcs REAL )

assume f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } ; :: thesis: f in Membership_Funcs REAL

then consider f1 being Function of REAL,REAL such that

B1: f = f1 and

B2: f1 is FuzzySet of REAL ;

thus f in Membership_Funcs REAL by B1, B2, Def1; :: thesis: verum

end;assume f in { f where f is Function of REAL,REAL : f is FuzzySet of REAL } ; :: thesis: f in Membership_Funcs REAL

then consider f1 being Function of REAL,REAL such that

B1: f = f1 and

B2: f1 is FuzzySet of REAL ;

thus f in Membership_Funcs REAL by B1, B2, Def1; :: thesis: verum