theorem Th12: :: MSAFREE:12

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 st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2