let Q be Quantale; :: thesis: for s being Element of Q

for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

let s be Element of Q; :: thesis: for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

let j be UnOp of Q; :: thesis: ( ( for a being Element of Q holds j . a = (a -r> s) -r> s ) implies j is monotone )

assume A1: for a being Element of Q holds j . a = (a -r> s) -r> s ; :: thesis: j is monotone

thus j is monotone :: thesis: verum

for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

let s be Element of Q; :: thesis: for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

let j be UnOp of Q; :: thesis: ( ( for a being Element of Q holds j . a = (a -r> s) -r> s ) implies j is monotone )

assume A1: for a being Element of Q holds j . a = (a -r> s) -r> s ; :: thesis: j is monotone

thus j is monotone :: thesis: verum

proof

let a, b be Element of Q; :: according to QUANTAL1:def 12 :: thesis: ( a [= b implies j . a [= j . b )

assume a [= b ; :: thesis: j . a [= j . b

then b -r> s [= a -r> s by Th13;

then A2: (a -r> s) -r> s [= (b -r> s) -r> s by Th13;

(a -r> s) -r> s = j . a by A1;

hence j . a [= j . b by A1, A2; :: thesis: verum

end;assume a [= b ; :: thesis: j . a [= j . b

then b -r> s [= a -r> s by Th13;

then A2: (a -r> s) -r> s [= (b -r> s) -r> s by Th13;

(a -r> s) -r> s = j . a by A1;

hence j . a [= j . b by A1, A2; :: thesis: verum