theorem Th68: :: NOMIN_1:68

for a1, a2, v1, v2 being object
for V, A being set st {v1,v2} c= V & v1 <> v2 & not v1 .--> a1 in A & not v2 .--> a2 in A & a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A holds
global_overlapping (V,A,(v1 .--> a1),(v2 .--> a2)) = (v2,v1) --> (a2,a1)