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 & b in X & c in X & a <> b & 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;