let n1, n2 be Element of NAT ; :: thesis: ( ex X being AntiChain_of_Prefixes of T st
( n1 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) & ex X being AntiChain_of_Prefixes of T st
( n2 = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) implies n1 = n2 )
given X1 being AntiChain_of_Prefixes of T such that A22: ( n1 = card X1 & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X1 ) ) ; :: thesis: ( for X being AntiChain_of_Prefixes of T holds
( not n2 = card X or ex Y being AntiChain_of_Prefixes of T st not card Y <= card X ) or n1 = n2 )
given X2 being AntiChain_of_Prefixes of T such that A23: ( n2 = card X2 & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X2 ) ) ; :: thesis: n1 = n2
( card X1 <= card X2 & card X2 <= card X1 ) by A22, A23;
hence n1 = n2 by A22, A23, XXREAL_0:1; :: thesis: verum