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:43
.= (id Y) | A by RELAT_1:94 ;
:: thesis: verum