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