:: deftheorem Def7 defines incl AOFA_L00:def 7 :
for X, Y being set st Y c= X holds
incl (Y,X) = id Y;