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

hereby :: thesis: ( (t . {} ) `1 in Vars implies t is non compound quasi-term of C )

assume t is non compound quasi-term of C ; :: thesis: (t . {} ) `1 in Vars
then consider x being Element of Vars such that
A1: t = x -term C by CompoundDef;
( t . {} = [x,a_Term ] & x in Vars ) by A1, TREES_4:3;
hence (t . {} ) `1 in Vars by MCART_1:7; :: thesis: verum

end;

assume (t . {} ) `1 in Vars ; :: thesis: t is non compound quasi-term of C
then ex x being Element of Vars st
( x = (t . {} ) `1 & t = x -term C ) by Th51;
hence t is non compound quasi-term of C ; :: thesis: verum