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