PFArt 1,k in PFBrt 1,k by Def4;
hence not PFBrt 1,k is empty ; :: thesis: verum