let fT be finite Tree; :: thesis: ( height fT = 0 implies fT = elementary_tree 0 )
assume A1: height fT = 0 ; :: thesis: fT = elementary_tree 0
thus fT c= elementary_tree 0 :: according to XBOOLE_0:def 10 :: thesis: elementary_tree 0 is_a_prefix_of fT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in fT or x in elementary_tree 0 )
assume A2: x in fT ; :: thesis: x in elementary_tree 0
reconsider t = x as Element of fT by A2;
A3: len t = 0 by A1, Def15;
A4: x = {} by A3;
thus x in elementary_tree 0 by A4, Th47; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in elementary_tree 0 or x in fT )
assume A5: x in elementary_tree 0 ; :: thesis: x in fT
A6: x = {} by A5, Th56, TARSKI:def 1;
thus x in fT by A6, Th47; :: thesis: verum