thus
id X is symmetric
:: thesis: ( id X is transitive & id X is antisymmetric )

proof

thus
id X is transitive
:: thesis: id X is antisymmetric
let a be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: for y being object 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 object ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X implies [b,a] in id X )

assume that

a in field (id X) and

b in field (id X) and

A1: [a,b] in id X ; :: thesis: [b,a] in id X

a = b by A1, RELAT_1:def 10;

hence [b,a] in id X by A1; :: thesis: verum

end;[y,a] in id X

let b be object ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X implies [b,a] in id X )

assume that

a in field (id X) and

b in field (id X) and

A1: [a,b] in id X ; :: thesis: [b,a] in id X

a = b by A1, RELAT_1:def 10;

hence [b,a] in id X by A1; :: thesis: verum

proof

thus
id X is antisymmetric
:: thesis: verum
let a be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being object 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 object ; :: 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 )

thus ( 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 ) by RELAT_1:def 10; :: thesis: verum

end;[a,z] in id X

let b, c be object ; :: 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 )

thus ( 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 ) by RELAT_1:def 10; :: thesis: verum

proof

let a be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being object 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 object ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b )

thus ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b ) by RELAT_1:def 10; :: thesis: verum

end;a = y

let b be object ; :: thesis: ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b )

thus ( a in field (id X) & b in field (id X) & [a,b] in id X & [b,a] in id X implies a = b ) by RELAT_1:def 10; :: thesis: verum