theorem Th2: :: PENCIL_1:2

for X being set holds
( 2 c= card X iff ex x, y being object st
( x in X & y in X & x <> y ) )