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