let Q be Subset of P; :: thesis: Q is oneone
Q ~ c= P ~ by SYSREL:11;
hence Q is oneone ; :: thesis: verum