set T = elementary_tree 0 ;

A1: 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
A2: Y c= X by Def14, Th56;
thus card Y <= card X by A2, NAT_1:44; :: thesis: verum

end;

thus width (elementary_tree 0 ) = 1 by A1, Def16; :: thesis: verum