theorem Th45: :: FLANG_1:45

for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *