:: deftheorem defines FI FUZIMPL1:def 15 :
FI = { f where f is Fuzzy_Implication : verum } ;