set f = (IsoCPRLSP X) " ;
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