theorem Th62: :: FIB_NUM2:62

for k being Nat holds (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))