let X, v be set ; ( 3 c= card X implies ex v1, v2 being set st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 ) )
assume
3 c= card X
; ex v1, v2 being set st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
then consider x, y, z being set such that
C:
x in X
and
D:
y in X
and
E:
z in X
and
F:
x <> y
and
G:
x <> z
and
H:
y <> z
by PENCIL_1:5;
( ( v <> x & v <> y & v <> z ) or v = x or v = y or v = z )
;
hence
ex v1, v2 being set st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
by C, D, E, F, G, H; verum