:: deftheorem defines are_conjugate FUZIMPL3:def 23 :
for f, g being UnOp of [.0,1.] holds
( f,g are_conjugate iff ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h) );