let F be Field; :: thesis: PRs F c= [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:]
let x be object ; :: 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 Def8; :: thesis: verum