let t be Integer; :: thesis: ( t is even & not 4 divides t implies ex u being Integer st

( u = t / 2 & u is odd ) )

assume A1: ( t is even & not 4 divides t ) ; :: thesis: ex u being Integer st

( u = t / 2 & u is odd )

then consider u being Integer such that

A2: t = 2 * u by ABIAN:11;

not 2 * 2 divides 2 * u by A1, A2;

then ( u = t / 2 & u is odd ) by A2, LmGCD;

hence ex u being Integer st

( u = t / 2 & u is odd ) ; :: thesis: verum

( u = t / 2 & u is odd ) )

assume A1: ( t is even & not 4 divides t ) ; :: thesis: ex u being Integer st

( u = t / 2 & u is odd )

then consider u being Integer such that

A2: t = 2 * u by ABIAN:11;

not 2 * 2 divides 2 * u by A1, A2;

then ( u = t / 2 & u is odd ) by A2, LmGCD;

hence ex u being Integer st

( u = t / 2 & u is odd ) ; :: thesis: verum