let t be finite Tree; :: thesis: for p being Element of t st t = t | p holds
p = {}
let p be Element of t; :: thesis: ( t = t | p implies p = {} )
( p <> {} implies height t > height (t | p) ) by TREES_1:48;
hence ( t = t | p implies p = {} ) ; :: thesis: verum