let A be MP-wff; :: thesis: ( not card (dom A) >= 2 or ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
set b = branchdeg (Root (dom A));
set a = Root (dom A);
assume A1: card (dom A) >= 2 ; :: thesis: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )

A2: now :: thesis: not branchdeg (Root (dom A)) = 0

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

end;

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

now :: thesis: ( ( branchdeg (Root (dom A)) = 1 & ex B being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ) or ( branchdeg (Root (dom A)) = 2 & ex B, C being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ) )

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

per cases then ( branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A2;

case A4: branchdeg (Root (dom A)) = 1 ; :: thesis: ex B being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )

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: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )

now :: thesis: ( A = 'not' B or A = (#) B )

per cases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A4, Def5;

suppose A . (Root (dom A)) = [1,0] ; :: thesis: ( A = 'not' B or A = (#) B )

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

end;

suppose A . (Root (dom A)) = [1,1] ; :: thesis: ( A = 'not' B or A = (#) B )

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

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: verum

end;

case A6: branchdeg (Root (dom A)) = 2 ; :: thesis: ex B, C being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )

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: ex C being MP-wff st
( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
take C = A | y; :: thesis: ( ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )
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: verum

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: verum