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