let a, b be Element of NAT ; :: thesis: ( ex A being Chain of Bottom L,x st a = card A & ( for A being Chain of Bottom L,x holds card A <= a ) & ex A being Chain of Bottom L,x st b = card A & ( for A being Chain of Bottom L,x holds card A <= b ) implies a = b )
assume ( ex A being Chain of Bottom L,x st a = card A & ( for A being Chain of Bottom L,x holds card A <= a ) & ex B being Chain of Bottom L,x st b = card B & ( for A being Chain of Bottom L,x holds card A <= b ) ) ; :: thesis: a = b
then ( a <= b & b <= a ) ;
hence a = b by XXREAL_0:1; :: thesis: verum