:: deftheorem Def4 defines Diagram ZF_FUND1:def 5 :
for H being ZF-formula
for E being non empty set
for b₃ being set holds
( b₃ = Diagram (H,E) iff for p being set holds
( p in b₃ iff ex f being Function of VAR,E st
( p = (f * decode) | (code (Free H)) & f in St (H,E) ) ) );