const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) axiom iff_trans: !P:prop.!Q:prop.!R:prop.(P <-> Q) -> (Q <-> R) -> (P <-> R) claim !x:set.!p:set prop.!q:set prop.!p2:set prop.PNoEq_ x p q -> PNoEq_ x q p2 -> !y:set.y iIn x -> (p y <-> p2 y)