let A be MP-wff; :: thesis: card (dom A) < card (dom ('not' A))
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;

now :: thesis: for s being FinSequence of NAT holds
( ( s in dom A implies o ^ s in dom ('not' A) ) & ( o ^ s in dom ('not' A) implies s in dom A ) )

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

now :: thesis: s in dom A

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: s in dom A

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

end;

suppose s <> {} ; :: thesis: s in dom A

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

end;

end;

end;

hence s in dom A ; :: thesis: verum

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