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 ^ s') where s' is Element of NAT * : o ^ s' in Z } ;
A2: ( Z | o,{ (o ^ s') where s' is Element of NAT * : o ^ s' in Z } are_equipotent & not Root Z in { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } ) by A1, Th25;
then reconsider A = { (o ^ s') where s' is Element of NAT * : o ^ s' in Z } as finite set by CARD_1:68;
reconsider B = A \/ {(Root Z)} as finite set ;
A3: card B = (card A) + 1 by A2, CARD_2:54
.= (card (Z | o)) + 1 by A2, CARD_1:21 ;
B c= Z

proof

now

let x be set ; :: thesis: ( x in B implies x in Z )
assume A4: x in B ; :: thesis: x in Z

now

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

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

then ex v' being Element of NAT * st
( x = o ^ v' & o ^ v' 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;

hence B c= Z by TARSKI:def 3; :: thesis: verum

end;

then (card (Z | o)) + 1 <= card Z by A3, NAT_1:44;
hence card (Z | o) < card Z by NAT_1:13; :: thesis: verum