const ordinal : set prop const Empty : set axiom ordinal_Empty: ordinal Empty const SNoLev : set set axiom ordinal_SNoLev: !x:set.ordinal x -> SNoLev x = x claim SNoLev Empty = Empty