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 )
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 )
set b = branchdeg (Root (dom A));
set a = Root (dom A);
A2: branchdeg (Root (dom A)) <= 2 by Def6;

A3: now

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

end;

now

per cases ( branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A2, A3, NAT_1:27;

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 13;
then consider x being set such that
A5: succ (Root (dom A)) = {x} by CARD_2:60;
x in succ (Root (dom A)) by A5, TARSKI:def 1;
then reconsider x' = x as Element of dom A ;
take B = A | x'; :: 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

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

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, Th28; :: 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, Th28; :: 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: Root A = [2,0 ] by Def6;
A8: succ (Root (dom A)) = {<*0 *>,<*1*>} by A6, Th24;
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 )
A = B '&' C by A7, A8, Th30;
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