take the odd square Element of NAT ; :: thesis: ( the odd square Element of NAT is odd & the odd square Element of NAT is square )
thus ( the odd square Element of NAT is odd & the odd square Element of NAT is square ) ; :: thesis: verum