let S be non empty non void ManySortedSign ; :: thesis:
let V be non-empty ManySortedSet of the carrier of S; :: thesis:
let X be non empty Subset of (S -Terms V); :: thesis:
set G = X -CircuitStr ;
let x be set ; :: thesis:

hereby :: thesis:

assume A1: x in InputVertices (X -CircuitStr) ; :: thesis:
then A2: not x in the carrier' of (X -CircuitStr) by XBOOLE_0:def 5;
thus x in Subtrees X by A1; :: thesis:
reconsider t = x as Term of S,V by A1, 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
A3: t . {} = [v,s] by A1, A2, Th5;
take s = s; :: thesis:
reconsider v = v as Element of V . s ;
take v = v; :: thesis:
thus x = root-tree [v,s] by A3, MSATERM:5; :: thesis:

end;

assume A4: x in Subtrees X ; :: thesis:
given s being SortSymbol of S, v being Element of V . s such that A5: x = root-tree [v,s] ; :: thesis:
assume not x in InputVertices (X -CircuitStr) ; :: thesis:
then x in the carrier' of (X -CircuitStr) by A4, XBOOLE_0:def 5;
then reconsider t = x as CompoundTerm of S,V by Th4;
t . {} = [v,s] by A5, 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:106;
then s in s ;
hence contradiction ; :: thesis: