:: deftheorem Def4 defines incl TOPREALC:def 4 :
for n being Nat
for T being non empty set
for R being real-membered set
for f being Function of T,R
for b₅ being Function of T,(TOP-REAL n) holds
( b₅ = incl (f,n) iff for t being Element of T holds b₅ . t = n |-> (f . t) );