const ordinal : set prop const SNo_ : set set prop const PSNo : set (set prop) set const In : set set prop term iIn = In infix iIn 2000 2000 axiom SNo_PSNo_eta_: !x:set.!y:set.ordinal x -> SNo_ x y -> y = PSNo x \z:set.z iIn y const SNo : set prop const SNoLev : set set axiom SNoLev_prop: !x:set.SNo x -> ordinal (SNoLev x) & SNo_ (SNoLev x) x claim !x:set.SNo x -> x = PSNo (SNoLev x) \y:set.y iIn x