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