A1: Membership_Funcs REAL c= { f where f is Function of REAL,REAL : f is FuzzySet of REAL }
proof
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;
{ f where f is Function of REAL,REAL : f is FuzzySet of REAL } c= Membership_Funcs REAL
proof
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;
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