:: deftheorem Def49 defines EGlobal_ MODELC_1:def 49 :
for S being non empty set
for R being total Relation of S,S
for b₃ being UnOp of (ModelSP S) holds
( b₃ = EGlobal_ R iff for f being object st f in ModelSP S holds
b₃ . f = EGlobal_0 (f,R) );