set J = (IsoCPNrSP (X,Y)) " ;
take (IsoCPNrSP (X,Y)) " ; :: thesis: ( (IsoCPNrSP (X,Y)) " is one-to-one & (IsoCPNrSP (X,Y)) " is onto & (IsoCPNrSP (X,Y)) " is isometric )
thus ( (IsoCPNrSP (X,Y)) " is one-to-one & (IsoCPNrSP (X,Y)) " is onto & (IsoCPNrSP (X,Y)) " is isometric ) ; :: thesis: verum