:: deftheorem defines ? FLANG_2:def 2 :
for E being set
for A being Subset of (E ^omega) holds A ? = union { B where B is Subset of (E ^omega) : ex k being Nat st
( k <= 1 & B = A |^ k ) } ;