theorem Th20: :: GLIBPRE0:16

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