let n, k be Element of NAT ; :: thesis: for x being set st x in PFBrt n,k holds
x is finite
let x be set ; :: thesis: ( x in PFBrt n,k implies x is finite )
assume x in PFBrt n,k ; :: thesis: x is finite
then A1: ( ex m being non empty Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) by Def4;

per cases ( ex m being Element of NAT st
( m <= n & x = PFArt m,k ) or x = PFCrt n,k ) by A1;

suppose ex m being Element of NAT st
( m <= n & x = PFArt m,k ) ; :: thesis: x is finite

then consider m being Element of NAT such that
A2: ( m <= n & x = PFArt m,k ) ;
thus x is finite by A2; :: thesis: verum

end;

suppose x = PFCrt n,k ; :: thesis: x is finite

hence x is finite ; :: thesis: verum

end;

end;