consider W being finite-branching DecoratedTree of such that
A1: ( W . {} = p & ( for x being Element of dom W
for w being Element of QC-WFF st w = W . x holds
succ W,x = list_of_immediate_constituents w ) ) from QC_LANG4:sch 1();
deffunc H₁( Element of QC-WFF ) -> Element of NAT = len (@ $1);
A2: for t, t' being Element of dom W
for d being Element of QC-WFF st t' in succ t & d = W . t' holds
H₁(d) < H₁(W . t)

proof

let t, t' be Element of dom W; :: thesis: for d being Element of QC-WFF st t' in succ t & d = W . t' holds
H₁(d) < H₁(W . t)
let d be Element of QC-WFF ; :: thesis: ( t' in succ t & d = W . t' implies H₁(d) < H₁(W . t) )
assume A3: ( t' in succ t & d = W . t' ) ; :: thesis: H₁(d) < H₁(W . t)
consider n being Element of NAT such that
A4: ( t' = t ^ <*n*> & t ^ <*n*> in dom W ) by A3;
dom (list_of_immediate_constituents (W . t)) = dom (succ W,t) by A1
.= dom (t succ ) by Th11 ;
then A5: n + 1 in dom (list_of_immediate_constituents (W . t)) by A4, Th12;
W . t' = (succ W,t) . (n + 1) by A4, Th13
.= (list_of_immediate_constituents (W . t)) . (n + 1) by A1 ;
hence H₁(d) < H₁(W . t) by A3, A5, Th30, QC_LANG2:71; :: thesis: verum

end;

W is finite from QC_LANG4:sch 2(A2);
then reconsider W = W as finite DecoratedTree of ;
take W ; :: thesis: ( W . {} = p & ( for x being Element of dom W holds succ W,x = list_of_immediate_constituents (W . x) ) )
thus ( W . {} = p & ( for x being Element of dom W holds succ W,x = list_of_immediate_constituents (W . x) ) ) by A1; :: thesis: verum