let fT be finite Tree; :: thesis: 1 <= width fT
( 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 ) ) & {{} } is AntiChain_of_Prefixes of fT ) by Def16, Th73;
then card {{} } <= width fT ;
hence 1 <= width fT by CARD_1:50; :: thesis: verum