A1: T <> {} ;
defpred S₁[ object , object ] means ex t1, t2 being Element of T st
( T = t1 & c₂ = t2 & t2 is_a_prefix_of t1 );
A2: for x, y being object st S₁[x,y] & S₁[y,x] holds
x = y by XBOOLE_0:def 10;
A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[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 S₁[y,x] ) ) from CARD_2:sch 1(A1, A2, A3);
reconsider x = x as Element of T by A4;

now :: thesis: for p being FinSequence of NAT st p in T holds
not x is_a_proper_prefix_of p

let p be FinSequence of NAT ; :: thesis: ( p in T implies not x is_a_proper_prefix_of p )
assume p in T ; :: thesis: not x is_a_proper_prefix_of p
then reconsider t1 = p as Element of T ;
thus not x is_a_proper_prefix_of p :: thesis: verum

proof

assume x is_a_prefix_of p ; :: according to XBOOLE_0:def 8 :: thesis: x = p
then x = t1 by A4;
hence x = p ; :: thesis: verum

end;

end;

hence ( Leaves T is finite & not Leaves T is empty ) by TREES_1:def 5; :: thesis: verum