theorem Th16: :: FIN_TOPO:16

for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^i) ` = A ^b