set n = the odd square Element of NAT ;
take the odd square Element of NAT ; :: thesis: ( not the odd square Element of NAT is even & the odd square Element of NAT is square )
thus ( not the odd square Element of NAT is even & the odd square Element of NAT is square ) ; :: thesis: verum