let A be MP-wff; :: thesis:
set b = branchdeg (Root (dom A));
set a = Root (dom A);
assume A1: card (dom A) >= 2 ; :: thesis:

A2: now :: thesis:

assume branchdeg (Root (dom A)) = 0 ; :: thesis:
then card (dom A) = 1 by Th12;
hence contradiction by A1; :: thesis:

end;

A3: branchdeg (Root (dom A)) <= 2 by Def5;

now :: thesis:

not not branchdeg (Root (dom A)) = 0 & ... & not branchdeg (Root (dom A)) = 2 by A3, NAT_1:60;

per cases by A2;

case A4: branchdeg (Root (dom A)) = 1 ; :: thesis:

then card (succ (Root (dom A))) = 1 by TREES_2:def 12;
then consider x being object such that
A5: succ (Root (dom A)) = {x} by CARD_2:42;
x in succ (Root (dom A)) by A5, TARSKI:def 1;
then reconsider x9 = x as Element of dom A ;
take B = A | x9; :: thesis:

now :: thesis:

per cases by A4, Def5;

suppose A . (Root (dom A)) = [1,0] ; :: thesis:

then Root A = [1,0] ;
hence ( A = 'not' B or A = (#) B ) by A5, Th18; :: thesis:

end;

suppose A . (Root (dom A)) = [1,1] ; :: thesis:

then Root A = [1,1] ;
hence ( A = 'not' B or A = (#) B ) by A5, Th18; :: thesis:

end;

end;

end;

hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; :: thesis:

end;

case A6: branchdeg (Root (dom A)) = 2 ; :: thesis:

then A7: 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 x = <*0*>, y = <*1*> as Element of dom A ;
take B = A | x; :: thesis:
take C = A | y; :: thesis:
Root A = [2,0] by A6, Def5;
then A = B '&' C by A7, Th20;
hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; :: thesis:

end;

end;

end;

hence ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; :: thesis: