:: deftheorem Def46 defines EneXt_ MODELC_1:def 46 :
for S being non empty set
for R being total Relation of S,S
for b₃ being UnOp of (ModelSP S) holds
( b₃ = EneXt_ R iff for f being object st f in ModelSP S holds
b₃ . f = EneXt_0 (f,R) );