let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_power_sets iff for X being set st X in E holds

E /\ (bool X) in E ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_power_sets iff for X being set st X in E holds

E /\ (bool X) in E )

hence ( E |= the_axiom_of_power_sets implies for X being set st X in E holds

E /\ (bool X) in E ) by Th8; :: thesis: ( ( for X being set st X in E holds

E /\ (bool X) in E ) implies E |= the_axiom_of_power_sets )

assume for X being set st X in E holds

E /\ (bool X) in E ; :: thesis: E |= the_axiom_of_power_sets

then for u being Element of E holds E /\ (bool u) in E ;

hence E |= the_axiom_of_power_sets by A1, Th8; :: thesis: verum

E /\ (bool X) in E ) )

assume A1: E is epsilon-transitive ; :: thesis: ( E |= the_axiom_of_power_sets iff for X being set st X in E holds

E /\ (bool X) in E )

hence ( E |= the_axiom_of_power_sets implies for X being set st X in E holds

E /\ (bool X) in E ) by Th8; :: thesis: ( ( for X being set st X in E holds

E /\ (bool X) in E ) implies E |= the_axiom_of_power_sets )

assume for X being set st X in E holds

E /\ (bool X) in E ; :: thesis: E |= the_axiom_of_power_sets

then for u being Element of E holds E /\ (bool u) in E ;

hence E |= the_axiom_of_power_sets by A1, Th8; :: thesis: verum