take IsoCPRLSP (X,Y) ; :: thesis: IsoCPRLSP (X,Y) is bijective
thus IsoCPRLSP (X,Y) is bijective ; :: thesis: verum