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 ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X ) ; :: thesis: a = b
hence a = b by RELAT_1:def 10; :: thesis: verum

end;

thus id X is reflexive :: thesis: verum

proof

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

end;