set x = the Element of X;
set y = the Element of X \ { the Element of X};
A3: ( [ the Element of X, the Element of X \ { the Element of X}] in [:X,X:] & [ the Element of X \ { the Element of X}, the Element of X] in [:X,X:] ) by ZFMISC_1:87;
then A4: ( the Element of X in field [:X,X:] & the Element of X \ { the Element of X} in field [:X,X:] ) by RELAT_1:15;
not the Element of X \ { the Element of X} in { the Element of X} by XBOOLE_0:def 5;
then the Element of X <> the Element of X \ { the Element of X} by TARSKI:def 1;
hence not [:X,X:] is antisymmetric by A3, A4, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum