let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for x being set holds
( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )
let X be non-empty ManySortedSet of S; :: thesis: for x being set holds
( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )
let x be set ; :: thesis: ( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )
TS (DTConOSA X) = union (rng (ParsedTerms X)) by Th8
.= Union the Sorts of (ParsedTermsOSA X) by CARD_3:def 4 ;
hence ( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) ) ; :: thesis: verum