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 Def13, Th37;
then card {{}} <= width fT ;
hence 1 <= width fT by CARD_1:30; :: thesis: verum