let A, B, C be MP-wff; ( 'not' A <> (#) B & 'not' A <> B '&' C )
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
set E = (elementary_tree 1) --> [1,0];
set F = (elementary_tree 1) --> [1,1];
reconsider e = {} as Element of dom ('not' A) by TREES_1:22;
A1:
( {} in dom ((#) B) & ( for u being FinSequence of NAT holds
( not u in dom B or not e = <*0*> ^ u or not ((#) B) . e = B . u ) ) )
by TREES_1:22;
A2:
<*0*> in elementary_tree 1
by TARSKI:def 2, TREES_1:51;
then A3:
<*0*> in dom ((elementary_tree 1) --> [1,0])
by FUNCOP_1:13;
then A4:
dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A))
by TREES_2:def 11;
A5:
<*0*> in dom ((elementary_tree 1) --> [1,1])
by A2, FUNCOP_1:13;
then
dom ((#) B) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom B))
by TREES_2:def 11;
then A6:
((#) B) . e = ((elementary_tree 1) --> [1,1]) . e
by A5, A1, TREES_2:def 11;
e in elementary_tree 1
by TREES_1:22;
then A7:
( ((elementary_tree 1) --> [1,0]) . e = [1,0] & ((elementary_tree 1) --> [1,1]) . e = [1,1] )
by FUNCOP_1:7;
( ( for u being FinSequence of NAT holds
( not u in dom A or not e = <*0*> ^ u or not ('not' A) . e = A . u ) ) & [1,0] <> [1,1] )
by XTUPLE_0:1;
hence
'not' A <> (#) B
by A3, A4, A6, A7, TREES_2:def 11; 'not' A <> B '&' C
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B);
A8:
( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> )
by TREES_1:28, TREES_1:52;
A9:
( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 )
by FUNCOP_1:13, TREES_1:28;
then
dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B))
by TREES_2:def 11;
then A10:
<*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))
by A9, A8, TREES_1:def 9;
then
dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) with-replacement (<*1*>,(dom C))
by TREES_2:def 11;
then A11:
<*1*> in dom (B '&' C)
by A10, TREES_1:def 9;
assume
not 'not' A <> B '&' C
; contradiction
then
ex s being FinSequence of NAT st
( s in dom A & <*1*> = <*0*> ^ s )
by A3, A4, A11, A12, TREES_1:def 9;
then
<*0*> is_a_prefix_of <*1*>
by TREES_1:1;
hence
contradiction
by TREES_1:3; verum