take IsoCPNrSP X ; :: thesis: ( IsoCPNrSP X is one-to-one & IsoCPNrSP X is onto & IsoCPNrSP X is isometric )
thus ( IsoCPNrSP X is one-to-one & IsoCPNrSP X is onto & IsoCPNrSP X is isometric ) ; :: thesis: verum