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

proof

consider x being object such that
A1: x in X by XBOOLE_0:def 1;
take x ; :: thesis: ( x in field (id X) & [x,x] in id X )
A2: field (id X) = (dom (id X)) \/ (rng (id X)) by RELAT_1:def 6;
thus x in field (id X) by A1, A2; :: thesis: [x,x] in id X
thus [x,x] in id X by A1, RELAT_1:def 10; :: thesis: verum

end;

hence not id X is irreflexive by RELAT_2:def 2, RELAT_2:def 10; :: thesis: verum