set t = o -term p;
( (o -term p) . {} = [o, the carrier of S] & the carrier of S in { the carrier of S} ) by TARSKI:def 1, TREES_4:def 4;
hence (o -term p) . {} in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87; :: according to ABCMIZ_1:def 27 :: thesis: o -term p is the_result_sort_of o -sort
thus o -term p is the_result_sort_of o -sort ; :: thesis: verum