let k be Nat; :: thesis: (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))
(2 * k) + 5 = (2 * (k + 2)) + 1 ;
then A1: (2 * k) + 5 in OddNAT ;
(2 * k) + 4 = 2 * ((k + 1) + 1) ;
then A2: {((2 * k) + 4)} misses OddNAT by Th52, ZFMISC_1:50;
OddNAT /\ (Seg ((2 * k) + 5)) = OddNAT /\ (Seg (((2 * k) + 4) + 1))
.= OddNAT /\ ((Seg ((2 * k) + 4)) \/ {((2 * k) + 5)}) by FINSEQ_1:9
.= (OddNAT /\ (Seg (((2 * k) + 3) + 1))) \/ (OddNAT /\ {((2 * k) + 5)}) by XBOOLE_1:23
.= (OddNAT /\ ((Seg ((2 * k) + 3)) \/ {((2 * k) + 4)})) \/ (OddNAT /\ {((2 * k) + 5)}) by FINSEQ_1:9
.= ((OddNAT /\ (Seg ((2 * k) + 3))) \/ (OddNAT /\ {((2 * k) + 4)})) \/ (OddNAT /\ {((2 * k) + 5)}) by XBOOLE_1:23
.= ((OddNAT /\ (Seg ((2 * k) + 3))) \/ {}) \/ (OddNAT /\ {((2 * k) + 5)}) by A2
.= (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} by A1, ZFMISC_1:46 ;
hence (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5)) ; :: thesis: verum