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