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

proof

dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . s in rng (coprod X) by FUNCT_1:def 3;
then A2: coprod (s,X) in rng (coprod X) by MSAFREE:def 3;
A3: Terminals (DTConOSA X) = Union (coprod X) by Th3;
set A1 = { aa where aa is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object 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 ) ) } ;
let x be object ; :: thesis: ( x in A iff S₁[x] )
thus ( x in A implies S₁[x] ) by A1; :: thesis: ( S₁[x] implies x in A )
assume S₁[x] ; :: thesis: x in A
then consider a being set such that
A4: a in X . s and
A5: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ;
A6: (ParsedTerms X) . s = ParsedTerms (X,s) by Def8;
set sa = [a,s];
[a,s] in coprod (s,X) by A4, MSAFREE:def 2;
then [a,s] in union (rng (coprod X)) by A2, TARSKI:def 4;
then A7: [a,s] in Terminals (DTConOSA X) by A3, 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 1;
b in { aa where aa is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object 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 ) ) } by A4;
then ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . b in the Sorts of (QuotOSAlg ((ParsedTermsOSA X),(LCongruence X))) . s by A6, FUNCT_2:5;
hence x in A by A1, A4, A5; :: thesis: verum

end;

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