let X be set ; :: thesis: ( id X is symmetric & id X is transitive )
thus id X is symmetric :: thesis: id X is transitive

proof

let a be set ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: for y being set st a in field (id X) & y in field (id X) & [a,y] in id X holds
[y,a] in id X
let b be set ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X implies [b,a] in id X )
assume A1: ( a in field (id X) & b in field (id X) & [a,b] in id X ) ; :: thesis: [b,a] in id X
then a = b by RELAT_1:def 10;
hence [b,a] in id X by A1; :: thesis: verum

end;

thus id X is transitive :: thesis: verum

proof

let a be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being set st a in field (id X) & y in field (id X) & z in field (id X) & [a,y] in id X & [y,z] in id X holds
[a,z] in id X
let b, c be set ; :: thesis: ( a in field (id X) & b in field (id X) & c in field (id X) & [a,b] in id X & [b,c] in id X implies [a,c] in id X )
assume ( a in field (id X) & b in field (id X) & c in field (id X) & [a,b] in id X & [b,c] in id X ) ; :: thesis: [a,c] in id X
hence [a,c] in id X by RELAT_1:def 10; :: thesis: verum

end;