let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in (id X) ~ iff [x,b] in id X )
let y be object ; :: thesis: ( [x,y] in (id X) ~ iff [x,y] in id X )
thus ( [x,y] in (id X) ~ implies [x,y] in id X ) :: thesis: ( [x,y] in id X implies [x,y] in (id X) ~ )

proof

assume [x,y] in (id X) ~ ; :: thesis: [x,y] in id X
then [y,x] in id X by Def5;
hence [x,y] in id X by Def8; :: thesis: verum

end;

assume A1: [x,y] in id X ; :: thesis: [x,y] in (id X) ~
then x = y by Def8;
hence [x,y] in (id X) ~ by A1, Def5; :: thesis: verum