for A being finite Chain
for n being Nat st card the carrier of A = n holds
A, InclPoset n are_isomorphic