let fT be finite Tree; :: thesis: 1 <= width fT
A1: ex X being AntiChain_of_Prefixes of fT st
( width fT = card X & ( for Y being AntiChain_of_Prefixes of fT holds card Y <= card X ) ) by Def16;
{{} } is AntiChain_of_Prefixes of fT by Th73;
then ( card {{} } <= width fT & card {{} } = 1 ) by A1, CARD_1:50;
hence 1 <= width fT ; :: thesis: verum