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