let A be MP-wff; :: thesis: ( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )
assume A1: card (dom A) = 1 ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )
A2: {} in dom A by TREES_1:47;
consider x being set such that
A3: dom A = {x} by A1, CARD_2:60;
A4: dom A = {{} } by A2, A3, TARSKI:def 1;
A5: dom A = elementary_tree 0 by A2, A3, TARSKI:def 1, TREES_1:56;
reconsider x = x as Element of dom A by A3, TARSKI:def 1;
succ x = {}

proof

A6: succ x = { (x ^ <*n*>) where n is Element of NAT : x ^ <*n*> in dom A } by TREES_2:def 5;
assume A7: not succ x = {} ; :: thesis: contradiction
consider y being Element of succ x;
y in succ x by A7;
then consider n being Element of NAT such that
A8: ( y = x ^ <*n*> & x ^ <*n*> in dom A ) by A6;
thus contradiction by A4, A8, TARSKI:def 1; :: thesis: verum

end;

then A9: branchdeg x = 0 by CARD_1:47, TREES_2:def 13;

now

per cases ( A . x = [0 ,0 ] or ex n being Element of NAT st A . x = [3,n] ) by A9, Def6;

suppose A . x = [0 ,0 ] ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )

then for z being set st z in dom A holds
A . z = [0 ,0 ] by A3, TARSKI:def 1;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) by A5, FUNCOP_1:17; :: thesis: verum

end;

suppose ex n being Element of NAT st A . x = [3,n] ; :: thesis: ( A = VERUM or ex p being MP-variable st A = @ p )

then consider n being Element of NAT such that
A10: A . x = [3,n] ;
A11: for z being set st z in dom A holds
A . z = [3,n] by A3, A10, TARSKI:def 1;
reconsider p = [3,n] as MP-variable by ZFMISC_1:128;
A = @ p by A5, A11, FUNCOP_1:17;
hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; :: thesis: verum

end;

end;

end;

hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; :: thesis: verum