theorem :: CARD_2:63

for x1, x2, x3, x4, x5 being object st x1,x2,x3,x4,x5 are_mutually_distinct holds
card {x1,x2,x3,x4,x5} = 5