set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
set SO = the Sorts of (ParsedTermsOSA X);
defpred S₁[ set ] means ex a being set st
( a in X . s & $1 = root-tree [a,s] );
consider A being set such that
A1: for x being set holds
( x in A iff ( x in the Sorts of (ParsedTermsOSA X) . s & S₁[x] ) ) from XBOOLE_0:sch 1();
A c= the Sorts of (ParsedTermsOSA X) . s

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the Sorts of (ParsedTermsOSA X) . s )
assume x in A ; :: thesis: x in the Sorts of (ParsedTermsOSA X) . s
hence x in the Sorts of (ParsedTermsOSA X) . s by A1; :: thesis: verum

end;

then reconsider A = A as Subset of (the Sorts of (ParsedTermsOSA X) . s) ;
for x being set holds
( x in A iff S₁[x] )

proof

let x be set ; :: thesis: ( x in A iff S₁[x] )
thus ( x in A implies S₁[x] ) by A1; :: thesis: ( S₁[x] implies x in A )
assume A2: S₁[x] ; :: thesis: x in A
then consider a being set such that
A3: ( a in X . s & x = root-tree [a,s] ) ;
A4: (ParsedTerms X) . s = ParsedTerms X,s by Def8;
set A1 = { aa where aa is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & aa = root-tree [x,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = aa . {} & the_result_sort_of o1 <= s ) ) } ;
set sa = [a,s];
A5: [a,s] in coprod s,X by A3, MSAFREE:def 2;
A6: Terminals (DTConOSA X) = Union (coprod X) by Th3;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . s in rng (coprod X) by FUNCT_1:def 5;
then coprod s,X in rng (coprod X) by MSAFREE:def 3;
then [a,s] in union (rng (coprod X)) by A5, TARSKI:def 4;
then A7: [a,s] in Terminals (DTConOSA X) by A6, CARD_3:def 4;
then reconsider sa = [a,s] as Symbol of (DTConOSA X) ;
reconsider b = root-tree sa as Element of TS (DTConOSA X) by A7, DTCONSTR:def 4;
( b in { aa where aa is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & aa = root-tree [x,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = aa . {} & the_result_sort_of o1 <= s ) ) } & b = x ) by A3;
hence x in A by A1, A2, A4; :: thesis: verum

end;

hence ex b₁ being Subset of (the Sorts of (ParsedTermsOSA X) . s) st
for x being set holds
( x in b₁ iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ; :: thesis: verum