let F be object ; :: according to TARSKI:def 3 :: thesis: ( not F in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } or F in Membership_Funcs REAL )
assume F in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } ; :: thesis: F in Membership_Funcs REAL
then consider f, g being Function of REAL,REAL such that
A1: F = f and
A2: for x being Real holds f . x = max (0,(min (1,(g . x)))) ;
F in { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } by A1, A2;
hence F in Membership_Funcs REAL by MM4, TARSKI:def 3; :: thesis: verum