let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A holds
( Psi q is one-to-one & Psi q is c=-monotone )
let q be Ideal of A; :: thesis: ( Psi q is one-to-one & Psi q is c=-monotone )
A1: for x1, x2 being object st x1 in dom (Psi q) & x2 in dom (Psi q) & (Psi q) . x1 = (Psi q) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (Psi q) & x2 in dom (Psi q) & (Psi q) . x1 = (Psi q) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (Psi q) & x2 in dom (Psi q) & (Psi q) . x1 = (Psi q) . x2 ) ; :: thesis: x1 = x2
then A3: ( x1 in Ideals (A / q) & x2 in Ideals (A / q) ) ;
then A4: x1 in { I where I is Ideal of (A / q) : verum } by RING_2:def 3;
x2 in { I where I is Ideal of (A / q) : verum } by A3, RING_2:def 3;
then consider z2 being Ideal of (A / q) such that
A5: z2 = x2 ;
consider z1 being Ideal of (A / q) such that
A6: z1 = x1 by A4;
A7: (canHom q) " z1 = (Psi q) . x2 by A2, Def3, A6
.= (canHom q) " z2 by A2, A5, Def3 ;
z1 = (canHom q) .: ((canHom q) " z2) by A7, Th24
.= z2 by Th24 ;
hence x1 = x2 by A5, A6; :: thesis: verum

end;

for x1, x2 being set st x1 in dom (Psi q) & x2 in dom (Psi q) & x1 c= x2 holds
(Psi q) . x1 c= (Psi q) . x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom (Psi q) & x2 in dom (Psi q) & x1 c= x2 implies (Psi q) . x1 c= (Psi q) . x2 )
assume A10: ( x1 in dom (Psi q) & x2 in dom (Psi q) & x1 c= x2 ) ; :: thesis: (Psi q) . x1 c= (Psi q) . x2
then A11: ( x1 in Ideals (A / q) & x2 in Ideals (A / q) ) ;
then A12: x1 in { I where I is Ideal of (A / q) : verum } by RING_2:def 3;
x2 in { I where I is Ideal of (A / q) : verum } by A11, RING_2:def 3;
then consider z2 being Ideal of (A / q) such that
A13: z2 = x2 ;
consider z1 being Ideal of (A / q) such that
A14: z1 = x1 by A12;
A15: (canHom q) " z1 = (Psi q) . x1 by A10, Def3, A14;
(canHom q) " z2 = (Psi q) . x2 by A10, A13, Def3;
hence (Psi q) . x1 c= (Psi q) . x2 by A15, A10, A13, A14, Th27; :: thesis: verum

end;

hence ( Psi q is one-to-one & Psi q is c=-monotone ) by A1, COHSP_1:def 11; :: thesis: verum