A1:
T <> {}
;
defpred S1[ object , object ] means ex t1, t2 being Element of T st
( T = t1 & c2 = t2 & t2 is_a_prefix_of t1 );
A2:
for x, y being object st S1[x,y] & S1[y,x] holds
x = y
by XBOOLE_0:def 10;
A3:
for x, y, z being object st S1[x,y] & S1[y,z] holds
S1[x,z]
by XBOOLE_1:1;
consider x being object such that
A4:
( x in T & ( for y being object st y in T & y <> x holds
not S1[y,x] ) )
from CARD_2:sch 1(A1, A2, A3);
reconsider x = x as Element of T by A4;
hence
( Leaves T is finite & not Leaves T is empty )
by TREES_1:def 5; verum