:: deftheorem Def15 defines Relax GRAPHSP:def 15 :
for n being Nat
for b₂ being Element of Funcs ((REAL *),(REAL *)) holds
( b₂ = Relax n iff ( dom b₂ = REAL * & ( for f being Element of REAL * holds b₂ . f = Relax (f,n) ) ) );