let X be set ; :: thesis:
assume 3 c= card X ; :: thesis:
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:

per cases ;

suppose ( x <> a & y <> a ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A1; :: thesis:

end;

suppose ( x <> a & y = a & x = b ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; :: thesis:

end;

suppose ( x <> a & y = a & x <> b ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; :: thesis:

end;

suppose ( x = a & y <> a & y = b ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A3, A5; :: thesis:

end;

suppose ( x = a & y <> a & y <> b ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; :: thesis:

end;

suppose ( x = a & y = a ) ; :: thesis:

hence ex z being set st
( z in X & x <> z & y <> z ) by A2, A4; :: thesis:

end;

end;