let X be set ; :: thesis: ( 3 c= card X implies for x, y being set ex z being set st
( z in X & x <> z & y <> z ) )
assume
3 c= card X
; :: thesis: for x, y being set ex z being set st
( z in X & x <> z & y <> z )
then consider a, b, c being set such that
A1:
a in X
and
A2:
b in X
and
A3:
c in X
and
A4:
a <> b
and
A5:
( a <> c & b <> c )
by Th5;
let x, y be set ; :: thesis: ex z being set st
( z in X & x <> z & y <> z )
per cases
( ( x <> a & y <> a ) or ( x <> a & y = a & x = b ) or ( x <> a & y = a & x <> b ) or ( x = a & y <> a & y = b ) or ( x = a & y <> a & y <> b ) or ( x = a & y = a ) )
;
end;