let X be set ; :: thesis: ( id X is antisymmetric & id X is reflexive )
thus id X is antisymmetric :: thesis: id X is reflexive

proof

let a be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being set st a in field (id X) & y in field (id X) & [a,y] in id X & [y,a] in id X holds
a = y
let b be set ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b )
assume that
a in field (id X) and
b in field (id X) and
A1: [a,b] in id X and
[b,a] in id X ; :: thesis: a = b
thus a = b by A1, RELAT_1:def 10; :: thesis: verum

end;

( id X is symmetric & id X is transitive ) by Th23;
hence id X is reflexive by Th22; :: thesis: verum