const In : set set prop term iIn = In infix iIn 2000 2000 const Power : set set const Subq : set set prop axiom PowerEq: !x:set.!y:set.y iIn Power x <-> Subq y x claim !x:set.!y:set.y iIn Power x -> Subq y x