let k be Element of 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 Th53, ZFMISC_1:56;
EvenNAT /\ (Seg ((2 * k) + 4)) = EvenNAT /\ (Seg (((2 * k) + 3) + 1))
.= EvenNAT /\ ((Seg ((2 * k) + 3)) \/ {((2 * k) + 4)}) by FINSEQ_1:11
.= (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:52
.= (EvenNAT /\ ((Seg ((2 * k) + 2)) \/ {((2 * k) + 3)})) \/ {((2 * k) + 4)} by FINSEQ_1:11
.= ((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, XBOOLE_0:def 7
.= (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} ;
hence (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4)) ; :: thesis: verum