theorem Th58: :: CARD_2:59

for x1, x2, x3, x4 being object st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
card {x1,x2,x3,x4} = 4