0 is even ;
then ze: 0 in EvenNAT by NUMERAL2:def 1;
let n be Nat; :: thesis: ( n is odd implies card (n /\ EvenNAT) = (n div 2) + 1 )
assume n: n is odd ; :: thesis: card (n /\ EvenNAT) = (n div 2) + 1
defpred S₁[ Nat] means ( $1 is odd implies card ($1 /\ EvenNAT) = ($1 div 2) + 1 );
i: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume k: for k being Nat st k < n holds
S₁[k] ; :: thesis: S₁[n]
assume nod: n is odd ; :: thesis: card (n /\ EvenNAT) = (n div 2) + 1
then reconsider no = n as odd Nat ;

per cases ( n >= 2 or n < 2 ) ;

suppose nd: n >= 2 ; :: thesis: card (n /\ EvenNAT) = (n div 2) + 1

then n >= 1 by XXREAL_0:2;
then reconsider nj = no - 1 as even Nat by NAT_1:21;
n - 1 < n - 0 by XREAL_1:15;
then njz: nj < n ;
nj >= 2 - 1 by nd, XREAL_1:9;
then reconsider nd = nj - 1 as odd Nat by NAT_1:21;
n - 2 < n - 0 by XREAL_1:15;
then ndz: nd < n ;
then tc: card (nd /\ EvenNAT) = (nd div 2) + 1 by k;
n - 2 < n - 1 by XREAL_1:15;
then njd: nd < nj ;
reconsider X = nd /\ EvenNAT as finite set ;
reconsider Y = n /\ EvenNAT as finite set ;
reconsider Z = {nd,nj} /\ EvenNAT as finite set ;
sen: Segm nd c= Segm n by ndz, NAT_1:39;
n = nd \/ {nj,nd}

proof

thus n c= nd \/ {nj,nd} :: according to XBOOLE_0:def 10 :: thesis: nd \/ {nj,nd} c= n

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in n or o in nd \/ {nj,nd} )
assume o in n ; :: thesis: o in nd \/ {nj,nd}
then os: o in Segm n ;
then reconsider on = o as Nat ;

per cases ( on < nd or on >= nd ) ;

suppose on < nd ; :: thesis: o in nd \/ {nj,nd}

then card (Segm on) in card (Segm nd) by NAT_1:41;
then on in nd ;
hence o in nd \/ {nj,nd} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose on: on >= nd ; :: thesis: o in nd \/ {nj,nd}

card (Segm on) in card (Segm n) by os;
then on < nj + 1 by NAT_1:41;
then on <= nd + 1 by NAT_1:13;
then ( on = nd or on = nj ) by on, NAT_1:9;
then on in {nd,nj} by TARSKI:def 2;
hence o in nd \/ {nj,nd} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus nd \/ {nj,nd} c= n :: thesis: verum

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in nd \/ {nj,nd} or o in n )
assume o in nd \/ {nj,nd} ; :: thesis: o in n
then ( o in nd or o in {nj,nd} ) by XBOOLE_0:def 3;

per cases then ( o in nd or o = nj or o = nd ) by TARSKI:def 2;

suppose o in nd ; :: thesis: o in n

hence o in n by sen; :: thesis: verum

end;

suppose on: o = nj ; :: thesis: o in n

card (Segm nj) in card (Segm n) by NAT_1:41, njz;
hence o in n by on; :: thesis: verum

end;

suppose on: o = nd ; :: thesis: o in n

card (Segm nd) in card (Segm n) by NAT_1:41, ndz;
hence o in n by on; :: thesis: verum

end;

end;

end;

end;

then xyz: Y = X \/ Z by XBOOLE_1:23;
X /\ Z = {}

proof

thus X /\ Z c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= X /\ Z

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in X /\ Z or o in {} )
assume o in X /\ Z ; :: thesis: o in {}
then ox: ( o in X & o in Z ) by XBOOLE_0:def 4;
then o in {nd,nj} by XBOOLE_0:def 4;

per cases then ( o = nd or o = nj ) by TARSKI:def 2;

suppose o = nd ; :: thesis: o in {}

then nd in nd by ox, XBOOLE_0:def 4;
hence o in {} ; :: thesis: verum

end;

suppose o = nj ; :: thesis: o in {}

then card (Segm nj) in card (Segm nd) by ox, XBOOLE_0:def 4;
hence o in {} by njd, NAT_1:41; :: thesis: verum

end;

end;

end;

thus {} c= X /\ Z by XBOOLE_1:2; :: thesis: verum

end;

then xmz: X misses Z by XBOOLE_0:def 7;
Z = {nj}

proof

thus Z c= {nj} :: according to XBOOLE_0:def 10 :: thesis: {nj} c= Z

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Z or o in {nj} )
assume o in Z ; :: thesis: o in {nj}
then ( o in {nd,nj} & o in EvenNAT ) by XBOOLE_0:def 4;
then oj: ( ( o = nd or o = nj ) & o in EvenNAT ) by TARSKI:def 2;
then consider oj being Nat such that
ojoj: ( oj = o & oj is even ) by NUMERAL2:def 1;
o = nj by oj, ojoj;
hence o in {nj} by TARSKI:def 1; :: thesis: verum

end;

thus {nj} c= Z :: thesis: verum

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in {nj} or o in Z )
assume o in {nj} ; :: thesis: o in Z
then o = nj by TARSKI:def 1;
then ( o in {nd,nj} & o in EvenNAT ) by TARSKI:def 2, NUMERAL2:def 1;
hence o in Z by XBOOLE_0:def 4; :: thesis: verum

end;

end;

then card Z = 1 by CARD_2:42;
hence card (n /\ EvenNAT) = ((nd div 2) + 1) + 1 by tc, xyz, xmz, CARD_2:40
.= (((nd - 1) / 2) + 1) + 1 by NAT_6:5
.= ((no - 1) / 2) + 1
.= (n div 2) + 1 by NAT_6:5 ;
:: thesis: verum

end;

suppose n < 2 ; :: thesis: card (n /\ EvenNAT) = (n div 2) + 1

then j: n = 1 by nod, NAT_1:23;
then n = {0} by CARD_1:49;
then n /\ EvenNAT = {0} by ze, ZFMISC_1:46;
hence card (n /\ EvenNAT) = ((no - 1) / 2) + 1 by j, CARD_1:30
.= (n div 2) + 1 by NAT_6:5 ;
:: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(i);
hence card (n /\ EvenNAT) = (n div 2) + 1 by n; :: thesis: verum