consider n being odd square Element of NAT ;
take n ; :: thesis: ( not n is even & n is square )
thus ( not n is even & n is square ) ; :: thesis: verum