theorem Th68: :: FLANG_1:68

for E being set
for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) * by ZFMISC_1:31, Th67;