let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for X being non empty Subset of (S -Terms V) holds
( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )
let X be non empty Subset of (S -Terms V); :: thesis: ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void )

hereby :: thesis: ( not X -CircuitStr is void implies X is SetWithCompoundTerm of S,V )

assume X is SetWithCompoundTerm of S,V ; :: thesis: not X -CircuitStr is void
then consider t being CompoundTerm of S,V such that
A1: t in X by MSATERM:def 7;
t . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def 6;
hence not X -CircuitStr is void by A1, TREES_9:25; :: thesis: verum

end;

assume not X -CircuitStr is void ; :: thesis: X is SetWithCompoundTerm of S,V
then consider t being Element of X such that
A2: ( not t is root or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by TREES_9:25;
t is CompoundTerm of S,V by A2, MSATERM:28, MSATERM:def 6;
hence X is SetWithCompoundTerm of S,V by MSATERM:def 7; :: thesis: verum