sy in [: the carrier' of S,{ the carrier of S}:] by Lm5;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A1: sy = [o,x2] by DOMAIN_1:1;
A2: x2 = the carrier of S by TARSKI:def 1;
then sy = Sym (o,V) by A1, MSAFREE:def 9;
hence sy -tree p is Term of S,V by A1, A2, Th1; :: thesis: verum