let W be Universe; :: thesis: W |= the_axiom_of_power_sets

now

let u be Element of W; :: thesis: W /\ (bool u) in W
W /\ (bool u) c= bool u by XBOOLE_1:17;
hence W /\ (bool u) in W by CLASSES1:def 1; :: thesis: verum

end;

hence W |= the_axiom_of_power_sets by ZFMODEL1:8; :: thesis: verum