let A be MP-wff; :: thesis:
set e = elementary_tree 1;
<*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
then A1: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
then A2: dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def 11;
then reconsider o = <*0*> as Element of dom ('not' A) by A1, TREES_1:def 9;

let s be FinSequence of NAT ; :: thesis:
thus ( s in dom A implies o ^ s in dom ('not' A) ) by A1, A2, TREES_1:def 9; :: thesis:
assume A3: o ^ s in dom ('not' A) ; :: thesis:

suppose s = {} ; :: thesis:

hence s in dom A by TREES_1:22; :: thesis:

end;

suppose s <> {} ; :: thesis:

then o is_a_proper_prefix_of o ^ s by TREES_1:10;
then ex w being FinSequence of NAT st
( w in dom A & o ^ s = o ^ w ) by A1, A2, A3, TREES_1:def 9;
hence s in dom A by FINSEQ_1:33; :: thesis:

end;

end;

end;

hence s in dom A ; :: thesis:

end;

then A4: dom A = (dom ('not' A)) | o by TREES_1:def 6;
o <> Root (dom ('not' A)) ;
hence card (dom A) < card (dom ('not' A)) by A4, Th16; :: thesis: