set T = elementary_tree 0;
now :: thesis: ex X being AntiChain_of_Prefixes of elementary_tree 0 st
( 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree 0 holds card Y <= card X ) )
reconsider X = {{}} as AntiChain_of_Prefixes of elementary_tree 0 by Th37;
take X = X; :: thesis: ( 1 = card X & ( for Y being AntiChain_of_Prefixes of elementary_tree 0 holds card Y <= card X ) )
thus 1 = card X by CARD_1:30; :: thesis: for Y being AntiChain_of_Prefixes of elementary_tree 0 holds card Y <= card X
let Y be AntiChain_of_Prefixes of elementary_tree 0; :: thesis: card Y <= card X
Y c= X by Def11, Th28;
hence card Y <= card X by NAT_1:43; :: thesis: verum
end;
hence width (elementary_tree 0) = 1 by Def13; :: thesis: verum