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