for A being Ordinal
for n being Nat st A,n are_equipotent holds
A = n by Lm4;