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