let X, Y be set ; :: thesis: ( X c= Y implies id X c= id Y )
assume X c= Y ; :: thesis: id X c= id Y
then X \/ Y = Y by XBOOLE_1:12;
then (id X) \/ (id Y) = id Y by Th14;
hence id X c= id Y by XBOOLE_1:7; :: thesis: verum