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