for X being set
for x being object holds
( card X = card {x} iff ex x being object st X = {x} ) by Th4, Th27;