set t = the CompoundTerm of S,V;
reconsider X = { the CompoundTerm of S,V} as non empty Subset of (S -Terms V) by ZFMISC_1:31;
take X ; :: thesis: ex t being CompoundTerm of S,V st t in X
take the CompoundTerm of S,V ; :: thesis: the CompoundTerm of S,V in X
thus the CompoundTerm of S,V in X by TARSKI:def 1; :: thesis: verum