let n, k be Element of NAT ; :: thesis: for x being set st x in PFBrt ((n + 1),k) holds
ex y being set st
( y in PFBrt (n,k) & y c= x )
let x be set ; :: thesis: ( x in PFBrt ((n + 1),k) implies ex y being set st
( y in PFBrt (n,k) & y c= x ) )
assume A1: x in PFBrt ((n + 1),k) ; :: thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )

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

suppose ex m being non zero Element of NAT st
( m <= n + 1 & x = PFArt (m,k) ) ; :: thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )

then consider m being non zero Element of NAT such that
A2: m <= n + 1 and
A3: x = PFArt (m,k) ;
thus ex y being set st
( y in PFBrt (n,k) & y c= x ) :: thesis: verum

proof

per cases ( m <= n or m = n + 1 ) by A2, NAT_1:8;

suppose A4: m <= n ; :: thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )

take y = x; :: thesis: ( y in PFBrt (n,k) & y c= x )
thus y in PFBrt (n,k) by A3, A4, Def4; :: thesis: y c= x
thus y c= x ; :: thesis: verum

end;

suppose A5: m = n + 1 ; :: thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )

take PFCrt (n,k) ; :: thesis: ( PFCrt (n,k) in PFBrt (n,k) & PFCrt (n,k) c= x )
n < n + 1 by NAT_1:13;
hence ( PFCrt (n,k) in PFBrt (n,k) & PFCrt (n,k) c= x ) by A3, A5, Def4, Lm7; :: thesis: verum

end;

end;

end;

end;

suppose A6: x = PFCrt ((n + 1),k) ; :: thesis: ex y being set st
( y in PFBrt (n,k) & y c= x )

take y = PFCrt (n,k); :: thesis: ( y in PFBrt (n,k) & y c= x )
thus y in PFBrt (n,k) by Def4; :: thesis: y c= x
thus y c= x by A6, Lm6; :: thesis: verum

end;

end;