let A, B, C be MP-wff; :: thesis: ( 'not' A <> (#) B & 'not' A <> B '&' C )
set e1 = elementary_tree 1;
set e2 = elementary_tree 2;
set E = (elementary_tree 1) --> [1,0 ];
set F = (elementary_tree 1) --> [1,1];
A1: <*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
A2: ( dom ((elementary_tree 1) --> [1,0 ]) = elementary_tree 1 & dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 ) by FUNCOP_1:19;
A3: ( <*0 *> in dom ((elementary_tree 1) --> [1,0 ]) & <*0 *> in dom ((elementary_tree 1) --> [1,1]) ) by A1, FUNCOP_1:19;
then A4: dom ('not' A) = (dom ((elementary_tree 1) --> [1,0 ])) with-replacement <*0 *>,(dom A) by TREES_2:def 12;
A5: dom ((#) B) = (dom ((elementary_tree 1) --> [1,1])) with-replacement <*0 *>,(dom B) by A3, TREES_2:def 12;
A6: ( {} in dom ('not' A) & {} in dom ((#) B) ) by TREES_1:47;
reconsider e = {} as Element of dom ('not' A) by TREES_1:47;
A7: for u being FinSequence of NAT holds
( not u in dom A or not e = <*0 *> ^ u or not ('not' A) . e = A . u ) ;
A8: e in elementary_tree 1 by TREES_1:47;
then A9: ((elementary_tree 1) --> [1,0 ]) . e = [1,0 ] by FUNCOP_1:13;
for u being FinSequence of NAT holds
( not u in dom B or not e = <*0 *> ^ u or not ((#) B) . e = B . u ) ;
then A10: ( not <*0 *> is_a_prefix_of e & ((#) B) . e = ((elementary_tree 1) --> [1,1]) . e ) by A3, A5, A6, TREES_2:def 12;
( ((elementary_tree 1) --> [1,1]) . e = [1,1] & [1,0 ] <> [1,1] ) by A8, FUNCOP_1:13, ZFMISC_1:33;
hence 'not' A <> (#) B by A3, A4, A7, A9, A10, TREES_2:def 12; :: thesis: 'not' A <> B '&' C
set y = ((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B;
A11: ( <*0 *> in elementary_tree 2 & <*1*> in elementary_tree 2 ) by TREES_1:55;
A12: dom ((elementary_tree 2) --> [2,0 ]) = elementary_tree 2 by FUNCOP_1:19;
then A13: dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B) = (dom ((elementary_tree 2) --> [2,0 ])) with-replacement <*0 *>,(dom B) by A11, TREES_2:def 12;
not <*0 *> is_a_proper_prefix_of <*1*> by TREES_1:89;
then A14: <*1*> in dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B) by A11, A12, A13, TREES_1:def 12;
then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0 ]) with-replacement <*0 *>,B)) with-replacement <*1*>,(dom C) by TREES_2:def 12;
then A15: <*1*> in dom (B '&' C) by A14, TREES_1:def 12;

A16: now

assume <*1*> in dom ((elementary_tree 1) --> [1,0 ]) ; :: thesis: contradiction
then ( <*1*> = {} or <*1*> = <*0 *> ) by A2, TARSKI:def 2, TREES_1:88;
hence contradiction by TREES_1:16; :: thesis: verum

end;

assume not 'not' A <> B '&' C ; :: thesis: contradiction
then ex s being FinSequence of NAT st
( s in dom A & <*1*> = <*0 *> ^ s ) by A3, A4, A15, A16, TREES_1:def 12;
then <*0 *> is_a_prefix_of <*1*> by TREES_1:8;
hence contradiction by TREES_1:16; :: thesis: verum