let X, Y be set ; :: thesis: ( id X c= id Y iff X c= Y )
thus ( id X c= id Y implies X c= Y ) :: thesis: ( X c= Y implies id X c= id Y )

proof

assume A1: id X c= id Y ; :: thesis: X c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume x in X ; :: thesis: x in Y
then [x,x] in id X by RELAT_1:def 10;
hence x in Y by A1, RELAT_1:def 10; :: thesis: verum

end;

assume A2: X c= Y ; :: thesis: id X c= id Y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in id X or z in id Y )
assume A3: z in id X ; :: thesis: z in id Y
then consider x, x9 being object such that
A4: x in X and
x9 in X and
A5: z = [x,x9] by ZFMISC_1:84;
x = x9 by A3, A5, RELAT_1:def 10;
hence z in id Y by A2, A4, A5, RELAT_1:def 10; :: thesis: verum