theorem Th5: :: PENCIL_1:5
for X being set holds
( 3 c= card X iff ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )