theorem Th26: :: MSATERM:26

for S being non empty non void ManySortedSign
for V1, V2 being non-empty ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2