theorem Th10: :: SCMYCIEL:10

for X being set holds card { {X,[x,X]} where x is Element of X : x in X } = card X