let n, k be Element of NAT ; :: thesis: not PFCrt (n,k) in PFBrt ((n + 1),k)
assume PFCrt (n,k) in PFBrt ((n + 1),k) ; :: thesis: contradiction
then ( ex m being non zero Element of NAT st
( m <= n + 1 & PFCrt (n,k) = PFArt (m,k) ) or PFCrt (n,k) = PFCrt ((n + 1),k) ) by Def4;
hence contradiction by Th17, Th18; :: thesis: verum