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