defpred S1[ object ] means ex a being set st
( a in X . s & \$1 = root-tree [a,s] );
set D = DTConMSA X;
consider A being set such that
A1: for x being object holds
( x in A iff ( x in () . s & S1[x] ) ) from A c= () . s by A1;
then reconsider A = A as Subset of (() . s) ;
for x being set holds
( x in A iff S1[x] )
proof
dom () = the carrier of S by PARTFUN1:def 2;
then (coprod X) . s in rng () by FUNCT_1:def 3;
then A2: coprod (s,X) in rng () by Def3;
A3: Terminals () = Union () by Th6;
let x be set ; :: thesis: ( x in A iff S1[x] )
thus ( x in A implies S1[x] ) by A1; :: thesis: ( S1[x] implies x in A )
set A = { aa where aa is Element of TS () : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) )
}
;
assume A4: S1[x] ; :: thesis: x in A
then consider a being set such that
A5: a in X . s and
A6: x = root-tree [a,s] ;
A7: (FreeSort X) . s = FreeSort (X,s) by Def11;
set sa = [a,s];
[a,s] in coprod (s,X) by ;
then [a,s] in union (rng ()) by ;
then A8: [a,s] in Terminals () by ;
then reconsider sa = [a,s] as Symbol of () ;
reconsider b = root-tree sa as Element of TS () by ;
b in { aa where aa is Element of TS () : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) )
}
by A5;
hence x in A by A1, A4, A6, A7; :: thesis: verum
end;
hence ex b1 being Subset of (() . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ; :: thesis: verum