theorem ThC1: :: MSAFREE5:70

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 holds
( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )