let C be initialized standardized ConstructorSignature; :: thesis: for t being expression of C holds
( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
let t be expression of C; :: thesis: ( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )

hereby :: thesis: ( ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) implies t is quasi-term of C )

assume t is quasi-term of C ; :: thesis: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars )
then reconsider tr = t as quasi-term of C ;
( tr is compound or not tr is compound ) ;
hence ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) by Th21, Th22; :: thesis: verum

end;

assume that
A1: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) and
A2: t is not quasi-term of C ; :: thesis: contradiction
A3: ( (t . {}) `1 in Vars implies ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) ) by Th17;
then ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) by A1, A2;
then ex o being OperSymbol of C st
( o = (t . {}) `1 & the_result_sort_of o = o `1 & t is expression of C, the_result_sort_of o ) by Th20;
hence contradiction by A2, A3, A1; :: thesis: verum