theorem :: FLANG_2:49

for E being set
for A being Subset of (E ^omega) holds A |^ (1,2) = A \/ (A ^^ A)