set T = elementary_tree 0;

now

reconsider X = {{}} as AntiChain_of_Prefixes of elementary_tree 0 by Th73;
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:50; :: 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 Def14, Th56;
hence card Y <= card X by NAT_1:44; :: thesis: verum

end;

hence width (elementary_tree 0) = 1 by Def16; :: thesis: verum