let t be Tree; :: thesis: for p being Element of t holds
( t | p = elementary_tree 0 iff p in Leaves t )
let p be Element of t; :: thesis: ( t | p = elementary_tree 0 iff p in Leaves t )
A1: not <*0*> in elementary_tree 0 by TARSKI:def 1, TREES_1:29;

hereby :: thesis: ( p in Leaves t implies t | p = elementary_tree 0 )

assume t | p = elementary_tree 0 ; :: thesis: p in Leaves t
then not p ^ <*0*> in t by A1, TREES_1:def 6;
hence p in Leaves t by TREES_1:54; :: thesis: verum

end;

assume A2: p in Leaves t ; :: thesis: t | p = elementary_tree 0
let q be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not q in t | p or q in elementary_tree 0 ) & ( not q in elementary_tree 0 or q in t | p ) )

hereby :: thesis: ( not q in elementary_tree 0 or q in t | p )

assume q in t | p ; :: thesis: q in elementary_tree 0
then p ^ q in t by TREES_1:def 6;
then A3: not p is_a_proper_prefix_of p ^ q by A2, TREES_1:def 5;
p is_a_prefix_of p ^ q by TREES_1:1;
then p ^ q = p by A3
.= p ^ {} by FINSEQ_1:34 ;
then q = {} by FINSEQ_1:33;
hence q in elementary_tree 0 by TREES_1:22; :: thesis: verum

end;

assume q in elementary_tree 0 ; :: thesis: q in t | p
then q = {} by TARSKI:def 1, TREES_1:29;
hence q in t | p by TREES_1:22; :: thesis: verum