let n, k be Element of NAT ; 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 ; ( 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)
; 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) )
;
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 )
verumproof
per cases
( m <= n or m = n + 1 )
by A2, NAT_1:8;
suppose A5:
m = n + 1
;
ex y being set st
( y in PFBrt (n,k) & y c= x )take
PFCrt (
n,
k)
;
( 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;
verum end; end;
end; end; end;