let S be OrderSortedSign; :: thesis: for X being V2() 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 V2() 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