theorem Th19: :: AOFA_L00:19

for I being set
for a being object holds pr1 (I,{a}) is one-to-one