:: deftheorem Def45 defines EneXt_0 MODELC_1:def 45 :
for S being non empty set
for R being total Relation of S,S
for f being object
for b₄ being Element of ModelSP S holds
( b₄ = EneXt_0 (f,R) iff for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b₄,S)) . s = TRUE ) );