:: deftheorem defines order SCMYCIEL:def 6 :
for X being finite finite-membered set holds order X = card (union X);