:: deftheorem defines card STRUCT_0:def 16 :
for S being 1-sorted holds card S = card the carrier of S;