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