let X, Y be set ; :: thesis: X /\ (Y --> X) = {}
assume X /\ (Y --> X) <> {} ; :: thesis: contradiction
then consider Z being object such that
A1: Z in X /\ (Y --> X) by XBOOLE_0:def 1;
reconsider Z = Z as set by TARSKI:1;
consider y, x being object such that
A2: ( y in Y & x in {X} & Z = [y,x] ) by ZFMISC_1:def 2, A1;
x = X by A2, TARSKI:def 1;
then Z = {{y,X},{y}} by A2, TARSKI:def 5;
then A3: {y,X} in Z by TARSKI:def 2;
( X in {y,X} & Z in X ) by A1, XBOOLE_0:def 4, TARSKI:def 2;
hence contradiction by A3, XREGULAR:7; :: thesis: verum