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 empty 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 Th20, Th21; :: thesis: verum