thus id X is symmetric :: thesis: ( id X is transitive & id X is antisymmetric )
proof
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;
thus id X is transitive :: thesis: id X is antisymmetric
proof
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;
thus id X is antisymmetric :: 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;