let X be set ; for v being object st 3 c= card X holds
ex v1, v2 being object st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
let v be object ; ( 3 c= card X implies ex v1, v2 being object st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 ) )
assume
3 c= card X
; ex v1, v2 being object st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
then consider x, y, z being object such that
A1:
x in X
and
A2:
y in X
and
A3:
z in X
and
A4:
x <> y
and
A5:
x <> z
and
A6:
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 object st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
by A1, A2, A3, A4, A5, A6; verum