:: deftheorem Def48 defines EGlobal_0 MODELC_1:def 48 :
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₄ = EGlobal_0 (f,R) iff for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b₄,S)) . s = TRUE ) );