defpred S1[ Nat] means for A being MP-wff st card (dom A) <= $1 holds
P1[A];
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: for A being MP-wff st card (dom A) <= k holds
P1[A] ; :: thesis: S1[k + 1]
let A be MP-wff; :: thesis: ( card (dom A) <= k + 1 implies P1[A] )
assume A8: card (dom A) <= k + 1 ; :: thesis: P1[A]
set a = Root (dom A);
set b = branchdeg (Root (dom A));
A9: branchdeg (Root (dom A)) <= 2 by Def5;
now :: thesis: P1[A]
not not branchdeg (Root (dom A)) = 0 & ... & not branchdeg (Root (dom A)) = 2 by A9, NAT_1:60;
per cases then ( branchdeg (Root (dom A)) = 0 or branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) ;
suppose A11: branchdeg (Root (dom A)) = 1 ; :: thesis: P1[A]
then A12: succ (Root (dom A)) = {<*0*>} by Th13;
then <*0*> in succ (Root (dom A)) by TARSKI:def 1;
then reconsider o = <*0*> as Element of dom A ;
A13: A = ((elementary_tree 1) --> (Root A)) with-replacement (<*0*>,(A | o)) by A12, Th18;
now :: thesis: P1[A]
per cases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A11, Def5;
suppose A14: A . (Root (dom A)) = [1,0] ; :: thesis: P1[A]
( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def 10;
then card (dom (A | o)) < k + 1 by A8, Th16, XXREAL_0:2;
then A15: card (dom (A | o)) <= k by NAT_1:13;
A = 'not' (A | o) by A13, A14;
hence P1[A] by A3, A7, A15; :: thesis: verum
end;
suppose A16: A . (Root (dom A)) = [1,1] ; :: thesis: P1[A]
( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def 10;
then card (dom (A | o)) < k + 1 by A8, Th16, XXREAL_0:2;
then A17: card (dom (A | o)) <= k by NAT_1:13;
A = (#) (A | o) by A13, A16;
hence P1[A] by A4, A7, A17; :: thesis: verum
end;
end;
end;
hence P1[A] ; :: thesis: verum
end;
suppose A18: branchdeg (Root (dom A)) = 2 ; :: thesis: P1[A]
then A19: succ (Root (dom A)) = {<*0*>,<*1*>} by Th14;
then ( <*0*> in succ (Root (dom A)) & <*1*> in succ (Root (dom A)) ) by TARSKI:def 2;
then reconsider o1 = <*0*>, o2 = <*1*> as Element of dom A ;
( dom (A | o1) = (dom A) | o1 & o1 <> Root (dom A) ) by TREES_2:def 10;
then card (dom (A | o1)) < k + 1 by A8, Th16, XXREAL_0:2;
then card (dom (A | o1)) <= k by NAT_1:13;
then A20: P1[A | o1] by A7;
( dom (A | o2) = (dom A) | o2 & o2 <> Root (dom A) ) by TREES_2:def 10;
then card (dom (A | o2)) < k + 1 by A8, Th16, XXREAL_0:2;
then card (dom (A | o2)) <= k by NAT_1:13;
then A21: P1[A | o2] by A7;
A = (((elementary_tree 2) --> (Root A)) with-replacement (<*0*>,(A | o1))) with-replacement (<*1*>,(A | o2)) by A19, Th20;
then A = (A | o1) '&' (A | o2) by A18, Def5;
hence P1[A] by A5, A20, A21; :: thesis: verum
end;
end;
end;
hence P1[A] ; :: thesis: verum
end;
let A be MP-wff; :: thesis: P1[A]
A22: card (dom A) <= card (dom A) ;
A23: S1[ 0 ] by NAT_1:2;
for n being Nat holds S1[n] from NAT_1:sch 2(A23, A6);
 hence P1[A] by A22; :: thesis: verum