let n1, n2 be 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 A32:
n1 = card X1
and
A33:
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 A34:
n2 = card X2
and
A35:
for Y being AntiChain_of_Prefixes of T holds card Y <= card X2
; n1 = n2
A36:
card X1 <= card X2
by A35;
card X2 <= card X1
by A33;
hence
n1 = n2
by A32, A34, A36, XXREAL_0:1; verum