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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in fT or x in elementary_tree 0 )
assume x in fT ; :: thesis: x in elementary_tree 0
then reconsider t = x as Element of fT ;
len t = 0 by A1, Def12;
then x = {} ;
hence x in elementary_tree 0 by Th21; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in elementary_tree 0 or x in fT )
assume x in elementary_tree 0 ; :: thesis: x in fT
then x = {} by Th28, TARSKI:def 1;
hence x in fT by Th21; :: thesis: verum