theorem Th63: :: FIB_NUM2:63

for k being Nat holds (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))