set J = (IsoCPNrSP X) " ;
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