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 zero 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

hence x is finite ; :: thesis: verum

end;

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

hence x is finite ; :: thesis: verum

end;

end;