let Z be finite Tree; :: thesis: for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z
let o be Element of Z; :: thesis: ( o <> Root Z implies card (Z | o) < card Z )
assume A1: o <> Root Z ; :: thesis: card (Z | o) < card Z
set A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ;
A2: Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A1, Th15;
then reconsider A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } as finite set by CARD_1:38;
reconsider B = A \/ {(Root Z)} as finite set ;

now :: thesis: for x being object st x in B holds
x in Z

let x be object ; :: thesis: ( x in B implies x in Z )
assume A3: x in B ; :: thesis: x in Z

now :: thesis: x in Z

per cases ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } or x in {(Root Z)} ) by A3, XBOOLE_0:def 3;

suppose x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; :: thesis: x in Z

then ex v9 being Element of NAT * st
( x = o ^ v9 & o ^ v9 in Z ) ;
hence x in Z ; :: thesis: verum

end;

suppose x in {(Root Z)} ; :: thesis: x in Z

hence x in Z ; :: thesis: verum

end;

end;

end;

hence x in Z ; :: thesis: verum

end;

then A4: B c= Z ;
card B = (card A) + 1 by A1, Th15, CARD_2:41
.= (card (Z | o)) + 1 by A2, CARD_1:5 ;
then (card (Z | o)) + 1 <= card Z by A4, NAT_1:43;
hence card (Z | o) < card Z by NAT_1:13; :: thesis: verum