ex x being object st
( x in field [:X,X:] & [x,x] in [:X,X:] )

proof

consider x being object such that
A3: x in X by XBOOLE_0:def 1;
take x ; :: thesis: ( x in field [:X,X:] & [x,x] in [:X,X:] )
field [:X,X:] = X \/ X by WELLSET1:2;
hence x in field [:X,X:] by A3; :: thesis: [x,x] in [:X,X:]
thus [x,x] in [:X,X:] by A3, ZFMISC_1:def 2; :: thesis: verum

end;

hence ( not [:X,X:] is irreflexive & not [:X,X:] is asymmetric ) by RELAT_2:def 2, RELAT_2:def 10; :: thesis: verum