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