let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1, M2 being Ideal of (A / q) holds
( M1 <> M2 iff (canHom q) " M1 <> (canHom q) " M2 )
let q be Ideal of A; :: thesis: for M1, M2 being Ideal of (A / q) holds
( M1 <> M2 iff (canHom q) " M1 <> (canHom q) " M2 )
let M1, M2 be Ideal of (A / q); :: thesis: ( M1 <> M2 iff (canHom q) " M1 <> (canHom q) " M2 )
( M1 <> M2 implies (canHom q) " M1 <> (canHom q) " M2 )

proof

assume A2: M1 <> M2 ; :: thesis: (canHom q) " M1 <> (canHom q) " M2
assume (canHom q) " M1 = (canHom q) " M2 ; :: thesis: contradiction
then M1 = (canHom q) .: ((canHom q) " M2) by Th24
.= M2 by Th24 ;
hence contradiction by A2; :: thesis: verum

end;

hence ( M1 <> M2 iff (canHom q) " M1 <> (canHom q) " M2 ) ; :: thesis: verum