:: deftheorem defines Theta FUZIMPL3:def 1 :
Theta = { f where f is bijective increasing UnOp of [.0,1.] : verum } ;