set a = the ordinal number ;
take <% the ordinal number %> ; :: thesis: ( <% the ordinal number %> is decreasing & <% the ordinal number %> is increasing & <% the ordinal number %> is non-decreasing & <% the ordinal number %> is non-increasing & <% the ordinal number %> is finite & not <% the ordinal number %> is empty )
thus ( <% the ordinal number %> is decreasing & <% the ordinal number %> is increasing & <% the ordinal number %> is non-decreasing & <% the ordinal number %> is non-increasing & <% the ordinal number %> is finite & not <% the ordinal number %> is empty ) ; :: thesis: verum