defpred S₁[ Nat] means for A being MP-wff st card (dom A) <= $1 holds
P₁[A];
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: for A being MP-wff st card (dom A) <= k holds
P₁[A] ; :: thesis: S₁[k + 1]
let A be MP-wff; :: thesis: ( card (dom A) <= k + 1 implies P₁[A] )
assume A8: card (dom A) <= k + 1 ; :: thesis: P₁[A]
set a = Root (dom A);
set b = branchdeg (Root (dom A));
A9: branchdeg (Root (dom A)) <= 2 by Def5;

now :: thesis: P₁[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 branchdeg (Root (dom A)) = 0 ; :: thesis: P₁[A]

then A10: card (dom A) = 1 by Th12;

now :: thesis: P₁[A]

per cases ( A = VERUM or ex p being MP-variable st A = @ p ) by A10, Th31;

suppose A = VERUM ; :: thesis: P₁[A]

hence P₁[A] by A1; :: thesis: verum

end;

suppose ex p being MP-variable st A = @ p ; :: thesis: P₁[A]

hence P₁[A] by A2; :: thesis: verum

end;

end;

end;

hence P₁[A] ; :: thesis: verum

end;

suppose A11: branchdeg (Root (dom A)) = 1 ; :: thesis: P₁[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: P₁[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: P₁[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 P₁[A] by A3, A7, A15; :: thesis: verum

end;

suppose A16: A . (Root (dom A)) = [1,1] ; :: thesis: P₁[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 P₁[A] by A4, A7, A17; :: thesis: verum

end;

end;

end;

hence P₁[A] ; :: thesis: verum

end;

suppose A18: branchdeg (Root (dom A)) = 2 ; :: thesis: P₁[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: P₁[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: P₁[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 P₁[A] by A5, A20, A21; :: thesis: verum

end;

end;

end;

hence P₁[A] ; :: thesis: verum

end;

let A be MP-wff; :: thesis: P₁[A]
A22: card (dom A) <= card (dom A) ;
A23: S₁[ 0 ] by NAT_1:2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A23, A6);
hence P₁[A] by A22; :: thesis: verum