:: deftheorem defines INT-ElemIns AOFA_I00:def 26 :
for X being non empty set holds INT-ElemIns X = [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];