PRs F c= [:(C3 F),(C3 F),(C3 F),(C3 F):] by Th13;
hence PRs F is Relation4 of C3 F by Def5; :: thesis: verum