take N ; :: thesis: ( not N is empty & N is ordinal )
thus ( not N is empty & N is ordinal ) ; :: thesis: verum