let A, Y be set ; :: thesis: ( A c= Y implies id A = (id Y) | A )
assume A c= Y ; :: thesis: id A = (id Y) | A
hence id A = id (Y /\ A) by XBOOLE_1:28
.= (id Y) * (id A) by FUNCT_1:22
.= (id Y) | A by RELAT_1:65 ;
:: thesis: verum