let F be Field; :: thesis: PRs F c= [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PRs F or x in [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] )
4C_3 F = [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] ;
hence ( not x in PRs F or x in [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] ) by Def9; :: thesis: verum