theorem Th57: :: FIB_NUM2:57

for k being Nat holds (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))