theorem Th8: :: ZFMODEL1:8

for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )