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:45;
let x be set ; :: thesis:

hereby :: thesis:

assume A2: x in InputVertices (X -CircuitStr) ; :: thesis:
then A3: 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 A2, 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:106;
then s in s ;
hence contradiction ; :: thesis: