theorem :: AOFA_A00:14

for X being set
for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object st a1 in X & a2 in X & a3 in X & a4 in X & a5 in X & a6 in X & a7 in X & a8 in X & a9 in X holds
{a1,a2,a3,a4,a5,a6,a7,a8,a9} c= X by ENUMSET1:def 7;