theorem Th28: :: FLANG_1:28

for E being set
for n being Nat holds {(<%> E)} |^ n = {(<%> E)}