:: deftheorem Def16 defines global_overlapping NOMIN_1:def 16 :
for V, A being set
for d1, d2 being object st d1 is TypeSCNominativeData of V,A & d2 is TypeSCNominativeData of V,A holds
for b₅ being TypeSCNominativeData of V,A holds
( ( not d1 in A & not d2 in A implies ( b₅ = global_overlapping (V,A,d1,d2) iff ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & b₅ = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) ) ) & ( ( d1 in A or d2 in A ) implies ( b₅ = global_overlapping (V,A,d1,d2) iff b₅ = d2 ) ) );