let S be non empty non void ManySortedSign ; :: thesis:
let V be V5 ManySortedSet of the carrier of S; :: thesis:
let X be non empty Subset of (S -Terms V); :: thesis:
set G = X -CircuitStr ;
A1: rng the ResultSort of (X -CircuitStr ) = the carrier' of (X -CircuitStr ) by RELAT_1:71;
let x be set ; :: thesis:

hereby :: thesis:

assume A2: x in InputVertices (X -CircuitStr ) ; :: thesis:
then A3: ( x in the carrier of (X -CircuitStr ) & not x in the carrier' of (X -CircuitStr ) ) by A1, XBOOLE_0:def 5;
thus x in Subtrees X by A2; :: thesis:
reconsider t = x as Term of S,V by A2, Th4;
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] ) by MSATERM:2;
then ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t is CompoundTerm of S,V ) by MSATERM:def 6;
then consider s being SortSymbol of S, v being Element of V . s such that
A4: t . {} = [v,s] by A3, Th5;
take s = s; :: thesis:
reconsider v = v as Element of V . s ;
take v = v; :: thesis:
thus x = root-tree [v,s] by A4, MSATERM:5; :: thesis:

end;

assume A5: x in Subtrees X ; :: thesis:
given s being SortSymbol of S, v being Element of V . s such that A6: x = root-tree [v,s] ; :: thesis:
assume not x in InputVertices (X -CircuitStr ) ; :: thesis:
then x in the carrier' of (X -CircuitStr ) by A1, A5, XBOOLE_0:def 5;
then reconsider t = x as CompoundTerm of S,V by Th4;
t . {} = [v,s] by A6, TREES_4:3;
then [v,s] in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6;
then s = the carrier of S by ZFMISC_1:129;
then s in s ;
hence contradiction ; :: thesis: