reconsider IT = <* the Element of A*> as FinSequence of A ;
take IT ; :: thesis: ( not IT is empty & IT is one-to-one & IT is ascending & IT is weakly-ascending & IT is descending & IT is weakly-descending )
thus ( not IT is empty & IT is one-to-one & IT is ascending & IT is weakly-ascending & IT is descending & IT is weakly-descending ) ; :: thesis: verum