theorem Th6: :: AOFA_A00:6

for I being non empty set
for i, j being Element of I
for x being set holds
( (i -singleton x) . i = {x} & ( i <> j implies (i -singleton x) . j = {} ) )