let A, B be MP-wff; :: thesis:
set e2 = elementary_tree 2;
set e1 = elementary_tree 1;
A1: dom VERUM = elementary_tree 0 by FUNCOP_1:13;
set F = (elementary_tree 1) --> [1,1];
set E = (elementary_tree 1) --> [1,0];
A2: <*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
then <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13;
then ( dom ((elementary_tree 1) --> [1,0]) = elementary_tree 1 & dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) ) by FUNCOP_1:13, TREES_2:def 11;
then <*0*> in dom ('not' A) by A2, TREES_1:def 9;
hence VERUM <> 'not' A by A1, TARSKI:def 1, TREES_1:29; :: thesis:
<*0*> in dom ((elementary_tree 1) --> [1,1]) by A2, FUNCOP_1:13;
then ( dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 & dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) ) by FUNCOP_1:13, TREES_2:def 11;
then <*0*> in dom ((#) A) by A2, TREES_1:def 9;
hence VERUM <> (#) A by A1, TARSKI:def 1, TREES_1:29; :: thesis:
set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A);
A3: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52;
A4: ( <*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*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def 11;
then A5: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A3, TREES_1:def 9;
then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def 11;
then A6: <*1*> in dom (A '&' B) by A5, TREES_1:def 9;
assume not VERUM <> A '&' B ; :: thesis:
hence contradiction by A1, A6, TARSKI:def 1, TREES_1:29; :: thesis: