let n1, n2 be Element of NAT ; ( 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 A52:
n1 = card X1
and
A53:
for Y being AntiChain_of_Prefixes of T holds card Y <= card X1
; ( 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 A54:
n2 = card X2
and
A55:
for Y being AntiChain_of_Prefixes of T holds card Y <= card X2
; n1 = n2
A56:
card X1 <= card X2
by A55;
card X2 <= card X1
by A53;
hence
n1 = n2
by A52, A54, A56, XXREAL_0:1; verum