deffunc H₃( Element of [:(LTLB_WFF **),(LTLB_WFF **):]) -> Enumeration of compn $1 = the Enumeration of compn $1;
ex T being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] st
( T . {} = P & ( for t being Element of dom T
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = T . t holds
succ (T,t) = H₃(w) ) ) from TREES_9:sch 2();
hence ex b₁ being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] st
( b₁ . {} = P & ( for t being Element of dom b₁
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b₁ . t holds
succ (b₁,t) = the Enumeration of compn w ) ) ; :: thesis: verum