:: deftheorem defines size SCMYCIEL:def 7 :
for X being finite set holds size X = card (PairsOf X);