theorem Th4: :: AOFA_A01:4

for I being non empty set
for a, b, c, d being set
for i, j being Element of I holds
( c in ((i -singleton a) (\/) (j -singleton d)) . b iff ( ( b = i & c = a ) or ( b = j & c = d ) ) )