theorem :: NOMIN_1:67

for a1, a2, v being object
for V, A being set st v in V & not v .--> a1 in A & not v .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds
global_overlapping (V,A,(v .--> a1),(v .--> a2)) = v .--> a2