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

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;