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